let L1, L2 be Lattice; :: thesis: for f being Function of the carrier of L1,the carrier of L2 holds
( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
let f be Function of the carrier of L1,the carrier of L2; :: thesis: ( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
A1: ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 implies f is Homomorphism of L1,L2 )

proof

assume ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) ; :: thesis: f is Homomorphism of L1,L2
then for a, b being Element of L1 holds
( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) ) by Def8, Def9;
hence f is Homomorphism of L1,L2 by LATTICE4:def 1; :: thesis: verum

end;

( f is Homomorphism of L1,L2 implies ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )

proof

assume f is Homomorphism of L1,L2 ; :: thesis: ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 )
then for a, b being Element of L1 holds
( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) ) by LATTICE4:def 1;
hence ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) by Def8, Def9; :: thesis: verum

end;

hence ( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) ) by A1; :: thesis: verum