let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of 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 ; :: 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 )
set H = product J;
A2: for i being Element of I holds J . i is Semilattice by A1;
A3: for i being Element of I holds J . i is complete LATTICE by A1;
then reconsider H = product J as complete LATTICE by WAYBEL_3:31;
H = H ;
hence ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def 19 :: thesis: for b₁ being Element of the carrier of (product J) holds b₁ "/\" is lower_adjoint
let f be Element of (product J); :: thesis: f "/\" is lower_adjoint
reconsider g = f as Element of H ;
reconsider F = f "/\" as Function of H,H ;
F is sups-preserving

proof

let X be Subset of H; :: according to WAYBEL_0:def 33 :: thesis: F preserves_sup_of X
reconsider Y = F .: X, X' = X as Subset of (product J) ;
reconsider sX = sup X as Element of (product J) ;
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 (product J) ;
A4: ( dom f1 = I & dom f2 = I ) by WAYBEL_3:27;

now

let x be set ; :: 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 (f . i) "/\" is lower_adjoint by WAYBEL_1:def 19;
then (f . i) "/\" is sups-preserving by A5;
then A6: ( (f . i) "/\" preserves_sup_of pi X',i & ex_sup_of pi X',i,J . i ) by A5, WAYBEL_0:def 33, YELLOW_0:17;
f2 = g "/\" (sup X) by WAYBEL_1:def 18;
then A7: f2 . i = (f . i) "/\" (sX . i) by A2, Th11
.= (f . i) "/\" (sup (pi X',i)) by A3, WAYBEL_3:32
.= ((f . i) "/\" ) . (sup (pi X',i)) by WAYBEL_1:def 18
.= sup (((f . i) "/\" ) .: (pi X',i)) by A6, WAYBEL_0:def 31 ;
pi Y,i = ((f . i) "/\" ) .: (pi X',i)

proof

thus pi Y,i c= ((f . i) "/\" ) .: (pi X',i) :: according to XBOOLE_0:def 10 :: thesis: ((f . i) "/\" ) .: (pi X',i) c= pi Y,i

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in pi Y,i or a in ((f . i) "/\" ) .: (pi X',i) )
assume a in pi Y,i ; :: thesis: a in ((f . i) "/\" ) .: (pi X',i)
then consider f3 being Function such that
A8: ( f3 in Y & a = f3 . i ) by CARD_3:def 6;
reconsider f3 = f3 as Element of (product J) by A8;
consider h being set such that
A9: ( h in dom F & h in X & f3 = F . h ) by A8, FUNCT_1:def 12;
reconsider h = h as Element of (product J) by A9;
A10: f3 . i = (f "/\" h) . i by A9, WAYBEL_1:def 18
.= (f . i) "/\" (h . i) by A2, Th11
.= ((f . i) "/\" ) . (h . i) by WAYBEL_1:def 18 ;
h . i in pi X',i by A9, CARD_3:def 6;
hence a in ((f . i) "/\" ) .: (pi X',i) by A8, A10, FUNCT_2:43; :: thesis: verum

end;

thus ((f . i) "/\" ) .: (pi X',i) c= pi Y,i :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in ((f . i) "/\" ) .: (pi X',i) or b in pi Y,i )
assume b in ((f . i) "/\" ) .: (pi X',i) ; :: thesis: b in pi Y,i
then consider f4 being set such that
A11: ( f4 in dom ((f . i) "/\" ) & f4 in pi X',i & b = ((f . i) "/\" ) . f4 ) by FUNCT_1:def 12;
consider f5 being Function such that
A12: ( f5 in X' & f4 = f5 . i ) by A11, CARD_3:def 6;
reconsider f5 = f5 as Element of (product J) by A12;
A13: ((f . i) "/\" ) . f4 = (f . i) "/\" (f5 . i) by A12, WAYBEL_1:def 18
.= (f "/\" f5) . i by A2, Th11 ;
f "/\" f5 = (f "/\" ) . f5 by WAYBEL_1:def 18;
then f "/\" f5 in (f "/\" ) .: X by A12, FUNCT_2:43;
hence b in pi Y,i by A11, A13, CARD_3:def 6; :: thesis: verum

end;

end;

hence f1 . x = f2 . x by A3, A7, WAYBEL_3:32; :: thesis: verum

end;

hence "\/" (F .: X),H = F . ("\/" X,H) by A4, FUNCT_1:9; :: thesis: verum

end;

hence f "/\" is lower_adjoint by WAYBEL_1:18; :: thesis: verum