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 A2, WAYBEL_3:31;

H = H ;

hence ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def 19 :: thesis: for b_{1} being Element of the carrier of (product J) holds b_{1} "/\" 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 ;

A3: for i being Element of I holds J . i is Semilattice by A1;

F is sups-preserving

( 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 A2, WAYBEL_3:31;

H = H ;

hence ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def 19 :: thesis: for b

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 ;

A3: for i being Element of I holds J . i is Semilattice by A1;

F is sups-preserving

proof

hence
f "/\" is lower_adjoint
by WAYBEL_1:17; :: thesis: verum
let X be Subset of H; :: according to WAYBEL_0:def 33 :: thesis: F preserves_sup_of X

reconsider Y = F .: X, X9 = 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) ;

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

end;reconsider Y = F .: X, X9 = 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: now :: thesis: for x being object st x in dom f1 holds

f1 . x = f2 . x

( dom f1 = I & dom f2 = I )
by WAYBEL_3:27;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)

(f . i) "/\" is lower_adjoint by A5, WAYBEL_1:def 19;

then A20: (f . i) "/\" preserves_sup_of pi (X9,i) by A5, WAYBEL_0:def 33;

f2 = g "/\" (sup X) by WAYBEL_1:def 18;

then f2 . i = (f . i) "/\" (sX . i) by A3, Th11

.= (f . i) "/\" (sup (pi (X9,i))) by A2, WAYBEL_3:32

.= ((f . i) "/\") . (sup (pi (X9,i))) by WAYBEL_1:def 18

.= sup (((f . i) "/\") .: (pi (X9,i))) by A20, A6 ;

hence f1 . x = f2 . x by A2, A19, WAYBEL_3:32; :: thesis: verum

end;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

pi (Y,i) c= ((f . i) "/\") .: (pi (X9,i))
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 A8, CARD_3:def 6;

reconsider f5 = f5 as Element of (product J) by A10;

f "/\" f5 = (f "/\") . f5 by WAYBEL_1:def 18;

then A12: f "/\" f5 in (f "/\") .: X by A10, FUNCT_2:35;

((f . i) "/\") . f4 = (f . i) "/\" (f5 . i) by A11, WAYBEL_1:def 18

.= (f "/\" f5) . i by A3, Th11 ;

hence b in pi (Y,i) by A9, A12, CARD_3:def 6; :: thesis: verum

end;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 A8, CARD_3:def 6;

reconsider f5 = f5 as Element of (product J) by A10;

f "/\" f5 = (f "/\") . f5 by WAYBEL_1:def 18;

then A12: f "/\" f5 in (f "/\") .: X by A10, FUNCT_2:35;

((f . i) "/\") . f4 = (f . i) "/\" (f5 . i) by A11, WAYBEL_1:def 18

.= (f "/\" f5) . i by A3, Th11 ;

hence b in pi (Y,i) by A9, A12, CARD_3:def 6; :: thesis: verum

proof

then A19:
pi (Y,i) = ((f . i) "/\") .: (pi (X9,i))
by A7;
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 (product J) by A13;

consider h being object such that

A15: h in dom F and

A16: h in X and

A17: f3 = F . h by A13, FUNCT_1:def 6;

reconsider h = h as Element of (product J) by A15;

A18: h . i in pi (X9,i) by A16, CARD_3:def 6;

f3 . i = (f "/\" h) . i by A17, WAYBEL_1:def 18

.= (f . i) "/\" (h . i) by A3, Th11

.= ((f . i) "/\") . (h . i) by WAYBEL_1:def 18 ;

hence a in ((f . i) "/\") .: (pi (X9,i)) by A14, A18, FUNCT_2:35; :: thesis: verum

end;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 (product J) by A13;

consider h being object such that

A15: h in dom F and

A16: h in X and

A17: f3 = F . h by A13, FUNCT_1:def 6;

reconsider h = h as Element of (product J) by A15;

A18: h . i in pi (X9,i) by A16, CARD_3:def 6;

f3 . i = (f "/\" h) . i by A17, WAYBEL_1:def 18

.= (f . i) "/\" (h . i) by A3, Th11

.= ((f . i) "/\") . (h . i) by WAYBEL_1:def 18 ;

hence a in ((f . i) "/\") .: (pi (X9,i)) by A14, A18, FUNCT_2:35; :: thesis: verum

(f . i) "/\" is lower_adjoint by A5, WAYBEL_1:def 19;

then A20: (f . i) "/\" preserves_sup_of pi (X9,i) by A5, WAYBEL_0:def 33;

f2 = g "/\" (sup X) by WAYBEL_1:def 18;

then f2 . i = (f . i) "/\" (sX . i) by A3, Th11

.= (f . i) "/\" (sup (pi (X9,i))) by A2, WAYBEL_3:32

.= ((f . i) "/\") . (sup (pi (X9,i))) by WAYBEL_1:def 18

.= sup (((f . i) "/\") .: (pi (X9,i))) by A20, A6 ;

hence f1 . x = f2 . x by A2, A19, WAYBEL_3:32; :: thesis: verum

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