set h = the Homomorphism of L1,L2;
take the Homomorphism of L1,L2 ; :: thesis: for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "\/" b) = ( the Homomorphism of L1,L2 . a) "\/" ( the Homomorphism of L1,L2 . b)
thus for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "\/" b) = ( the Homomorphism of L1,L2 . a) "\/" ( the Homomorphism of L1,L2 . b) by LATTICE4:def 1; :: thesis: verum