let L1, L2 be Lattice; :: thesis: ( L1 is 01_Lattice & L2 is 01_Lattice implies ( ( L1 is pseudocomplemented & L2 is pseudocomplemented ) iff [:L1,L2:] is pseudocomplemented ) )
assume A0: ( L1 is 01_Lattice & L2 is 01_Lattice ) ; :: thesis: ( ( L1 is pseudocomplemented & L2 is pseudocomplemented ) iff [:L1,L2:] is pseudocomplemented )
thus ( L1 is pseudocomplemented & L2 is pseudocomplemented implies [:L1,L2:] is pseudocomplemented ) :: thesis: ( [:L1,L2:] is pseudocomplemented implies ( L1 is pseudocomplemented & L2 is pseudocomplemented ) )

proof

assume A1: ( L1 is pseudocomplemented & L2 is pseudocomplemented ) ; :: thesis: [:L1,L2:] is pseudocomplemented
for x being Element of [:L1,L2:] ex y being Element of [:L1,L2:] st y is_a_pseudocomplement_of x

proof

let x be Element of [:L1,L2:]; :: thesis: ex y being Element of [:L1,L2:] st y is_a_pseudocomplement_of x
consider x1, x2 being object such that
B1: ( x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of L1 by B1;
reconsider x2 = x2 as Element of L2 by B1;
consider xx1 being Element of L1 such that
A2: xx1 is_a_pseudocomplement_of x1 by A1;
consider xx2 being Element of L2 such that
A3: xx2 is_a_pseudocomplement_of x2 by A1;
take y = [xx1,xx2]; :: thesis: y is_a_pseudocomplement_of x
thus y is_a_pseudocomplement_of x by B1, A2, A3, ProductPsCompl, A0; :: thesis: verum

end;

hence [:L1,L2:] is pseudocomplemented ; :: thesis: verum

end;

assume aa: [:L1,L2:] is pseudocomplemented ; :: thesis: ( L1 is pseudocomplemented & L2 is pseudocomplemented )
for x being Element of L1 ex y being Element of L1 st y is_a_pseudocomplement_of x

proof

let x be Element of L1; :: thesis: ex y being Element of L1 st y is_a_pseudocomplement_of x
set x2 = the Element of L2;
consider y being Element of [:L1,L2:] such that
B0: y is_a_pseudocomplement_of [x, the Element of L2] by aa;
consider y1, y2 being object such that
B1: ( y1 in the carrier of L1 & y2 in the carrier of L2 & y = [y1,y2] ) by ZFMISC_1:def 2;
reconsider y1 = y1 as Element of L1 by B1;
reconsider y2 = y2 as Element of L2 by B1;
take y1 ; :: thesis: y1 is_a_pseudocomplement_of x
thus y1 is_a_pseudocomplement_of x by B1, B0, ProductPsCompl, A0; :: thesis: verum

end;

hence L1 is pseudocomplemented ; :: thesis: L2 is pseudocomplemented
for x being Element of L2 ex y being Element of L2 st y is_a_pseudocomplement_of x

proof

let x be Element of L2; :: thesis: ex y being Element of L2 st y is_a_pseudocomplement_of x
set x2 = the Element of L1;
consider y being Element of [:L1,L2:] such that
B0: y is_a_pseudocomplement_of [ the Element of L1,x] by aa;
consider y1, y2 being object such that
B1: ( y1 in the carrier of L1 & y2 in the carrier of L2 & y = [y1,y2] ) by ZFMISC_1:def 2;
reconsider y1 = y1 as Element of L1 by B1;
reconsider y2 = y2 as Element of L2 by B1;
take y2 ; :: thesis: y2 is_a_pseudocomplement_of x
thus y2 is_a_pseudocomplement_of x by B1, B0, ProductPsCompl, A0; :: thesis: verum

end;

hence L2 is pseudocomplemented ; :: thesis: verum