let L1, L2 be Lattice; :: thesis: for p1 being Element of L1
for p2 being Element of L2 st L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice holds
[p1,p2] * = [(p1 *),(p2 *)]
let p1 be Element of L1; :: thesis: for p2 being Element of L2 st L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice holds
[p1,p2] * = [(p1 *),(p2 *)]
let p2 be Element of L2; :: thesis: ( L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice implies [p1,p2] * = [(p1 *),(p2 *)] )
assume A1: ( L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice ) ; :: thesis: [p1,p2] * = [(p1 *),(p2 *)]
A3: p1 * is_a_pseudocomplement_of p1 by def3, A1;
p2 * is_a_pseudocomplement_of p2 by def3, A1;
then [(p1 *),(p2 *)] is_a_pseudocomplement_of [p1,p2] by A3, ProductPsCompl, A1;
hence [p1,p2] * = [(p1 *),(p2 *)] by def3, A1; :: thesis: verum