let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds
( product J is complete & product J is Heyting )

let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is complete Heyting LATTICE ) implies ( product J is complete & product J is Heyting ) )
assume A1: for i being Element of I holds J . i is complete Heyting LATTICE ; :: thesis: ( product J is complete & product J is Heyting )
A2: for i being Element of I holds J . i is complete LATTICE by A1;
set H = product J;
reconsider H = product J as complete LATTICE by ;
H = H ;
hence ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def 19 :: thesis: for b1 being Element of the carrier of () holds b1 "/\" is lower_adjoint
let f be Element of (); :: thesis:
reconsider g = f as Element of H ;
reconsider F = f "/\" as Function of H,H ;
A3: for i being Element of I holds J . i is Semilattice by A1;
F is sups-preserving
proof
let X be Subset of H; :: according to WAYBEL_0:def 33 :: thesis:
reconsider Y = F .: X, X9 = X as Subset of () ;
reconsider sX = sup X as Element of () ;
assume ex_sup_of X,H ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: X,H & "\/" ((F .: X),H) = F . ("\/" (X,H)) )
thus ex_sup_of F .: X,H by YELLOW_0:17; :: thesis: "\/" ((F .: X),H) = F . ("\/" (X,H))
reconsider f1 = sup (F .: X), f2 = F . (sup X) as Element of () ;
A4: now :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x
let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider i = x as Element of I by WAYBEL_3:27;
A5: J . i is complete Heyting LATTICE by A1;
then A6: ex_sup_of pi (X9,i),J . i by YELLOW_0:17;
A7: ((f . i) "/\") .: (pi (X9,i)) c= pi (Y,i)
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in ((f . i) "/\") .: (pi (X9,i)) or b in pi (Y,i) )
assume b in ((f . i) "/\") .: (pi (X9,i)) ; :: thesis: b in pi (Y,i)
then consider f4 being object such that
f4 in dom ((f . i) "/\") and
A8: f4 in pi (X9,i) and
A9: b = ((f . i) "/\") . f4 by FUNCT_1:def 6;
consider f5 being Function such that
A10: f5 in X9 and
A11: f4 = f5 . i by ;
reconsider f5 = f5 as Element of () by A10;
f "/\" f5 = (f "/\") . f5 by WAYBEL_1:def 18;
then A12: f "/\" f5 in (f "/\") .: X by ;
((f . i) "/\") . f4 = (f . i) "/\" (f5 . i) by
.= (f "/\" f5) . i by ;
hence b in pi (Y,i) by ; :: thesis: verum
end;
pi (Y,i) c= ((f . i) "/\") .: (pi (X9,i))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in pi (Y,i) or a in ((f . i) "/\") .: (pi (X9,i)) )
assume a in pi (Y,i) ; :: thesis: a in ((f . i) "/\") .: (pi (X9,i))
then consider f3 being Function such that
A13: f3 in Y and
A14: a = f3 . i by CARD_3:def 6;
reconsider f3 = f3 as Element of () by A13;
consider h being object such that
A15: h in dom F and
A16: h in X and
A17: f3 = F . h by ;
reconsider h = h as Element of () by A15;
A18: h . i in pi (X9,i) by ;
f3 . i = (f "/\" h) . i by
.= (f . i) "/\" (h . i) by
.= ((f . i) "/\") . (h . i) by WAYBEL_1:def 18 ;
hence a in ((f . i) "/\") .: (pi (X9,i)) by ; :: thesis: verum
end;
then A19: pi (Y,i) = ((f . i) "/\") .: (pi (X9,i)) by A7;
(f . i) "/\" is lower_adjoint by ;
then A20: (f . i) "/\" preserves_sup_of pi (X9,i) by ;
f2 = g "/\" (sup X) by WAYBEL_1:def 18;
then f2 . i = (f . i) "/\" (sX . i) by
.= (f . i) "/\" (sup (pi (X9,i))) by
.= ((f . i) "/\") . (sup (pi (X9,i))) by WAYBEL_1:def 18
.= sup (((f . i) "/\") .: (pi (X9,i))) by ;
hence f1 . x = f2 . x by ; :: thesis: verum
end;
( dom f1 = I & dom f2 = I ) by WAYBEL_3:27;
hence "\/" ((F .: X),H) = F . ("\/" (X,H)) by ; :: thesis: verum
end;
hence f "/\" is lower_adjoint by WAYBEL_1:17; :: thesis: verum