let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
let J be RelStr-yielding non-Empty ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies for i being Element of I holds (Top (product J)) . i = Top (J . i) )
assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; :: thesis: for i being Element of I holds (Top (product J)) . i = Top (J . i)
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Top (J . $1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch 5();
A3: now :: thesis: for i being Element of I holds f . i is Element of (J . i)
let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = Top (J . i) by A2;
hence f . i is Element of (J . i) ; :: thesis: verum
end;
dom f = I by PARTFUN1:def 2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
let i be Element of I; :: thesis: (Top (product J)) . i = Top (J . i)
A4: {} is_>=_than f ;
A5: now :: thesis: for c being Element of (product J) st {} is_>=_than c & ( for b being Element of (product J) st {} is_>=_than b holds
b <= c ) holds
c = f
let c be Element of (product J); :: thesis: ( {} is_>=_than c & ( for b being Element of (product J) st {} is_>=_than b holds
b <= c ) implies c = f )
assume that
{} is_>=_than c and
A6: for b being Element of (product J) st {} is_>=_than b holds
b <= c ; :: thesis: c = f
now :: thesis: for i being Element of I holds f . i >= c . i
let i be Element of I; :: thesis: f . i >= c . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= c . i by YELLOW_0:45; :: thesis: verum
end;
then A7: f >= c by WAYBEL_3:28;
for i being Element of I holds J . i is antisymmetric by A1;
then A8: product J is antisymmetric by WAYBEL_3:30;
c >= f by A6, YELLOW_0:6;
hence c = f by A8, A7; :: thesis: verum
end;
A9: now :: thesis: for a being Element of (product J) st {} is_>=_than a holds
f >= a
let a be Element of (product J); :: thesis: ( {} is_>=_than a implies f >= a )
assume {} is_>=_than a ; :: thesis: f >= a
now :: thesis: for i being Element of I holds f . i >= a . i
let i be Element of I; :: thesis: f . i >= a . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= a . i by YELLOW_0:45; :: thesis: verum
end;
hence f >= a by WAYBEL_3:28; :: thesis: verum
end;
now :: thesis: for b being Element of (product J) st {} is_>=_than b holds
f >= b
let b be Element of (product J); :: thesis: ( {} is_>=_than b implies f >= b )
assume {} is_>=_than b ; :: thesis: f >= b
now :: thesis: for i being Element of I holds f . i >= b . i
let i be Element of I; :: thesis: f . i >= b . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= b . i by YELLOW_0:45; :: thesis: verum
end;
hence f >= b by WAYBEL_3:28; :: thesis: verum
end;
then ex_inf_of {} , product J by A4, A5;
then f = "/\" ({},(product J)) by A4, A9, YELLOW_0:def 10;
hence (Top (product J)) . i = Top (J . i) by A2; :: thesis: verum