let L1, L2 be complete Lattice; :: thesis: for f being Function of the carrier of L1,the carrier of L2 st f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
let f be Function of the carrier of L1,the carrier of L2; :: thesis: ( f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) implies f is Homomorphism of L1,L2 )
assume A1: ( f is one-to-one & rng f = the carrier of L2 ) ; :: thesis: ( ex a, b being Element of L1 st
( ( a [= b implies f . a [= f . b ) implies ( f . a [= f . b & not a [= b ) ) or f is Homomorphism of L1,L2 )
assume A2: for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ; :: thesis: f is Homomorphism of L1,L2
A3: for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b)

proof

let a, b be Element of L1; :: thesis: f . (a "\/" b) = (f . a) "\/" (f . b)
A4: {(f . a),(f . b)} is_less_than f . (a "\/" b)

proof

( a [= a "\/" b & b [= a "\/" b ) by LATTICES:22;
then ( f . a [= f . (a "\/" b) & f . b [= f . (a "\/" b) ) by A2;
then for q being Element of L2 st q in {(f . a),(f . b)} holds
q [= f . (a "\/" b) by TARSKI:def 2;
hence {(f . a),(f . b)} is_less_than f . (a "\/" b) by LATTICE3:def 17; :: thesis: verum

end;

for r being Element of L2 st {(f . a),(f . b)} is_less_than r holds
f . (a "\/" b) [= r

proof

let r be Element of L2; :: thesis: ( {(f . a),(f . b)} is_less_than r implies f . (a "\/" b) [= r )
assume A5: {(f . a),(f . b)} is_less_than r ; :: thesis: f . (a "\/" b) [= r
( f . a in {(f . a),(f . b)} & f . b in {(f . a),(f . b)} ) by TARSKI:def 2;
then A6: ( f . a [= r & f . b [= r ) by A5, LATTICE3:def 17;
reconsider g = f " as Function of the carrier of L2,the carrier of L1 by A1, FUNCT_2:31;
A7: f . (g . r) = r by A1, FUNCT_1:57;
then ( a [= g . r & b [= g . r ) by A2, A6;
then for q being Element of L1 st q in {a,b} holds
q [= g . r by TARSKI:def 2;
then A8: {a,b} is_less_than g . r by LATTICE3:def 17;
a "\/" b = "\/" {a,b} by LATTICE3:44;
then a "\/" b [= g . r by A8, LATTICE3:def 21;
hence f . (a "\/" b) [= r by A2, A7; :: thesis: verum

end;

then f . (a "\/" b) = "\/" {(f . a),(f . b)},L2 by A4, LATTICE3:def 21;
hence f . (a "\/" b) = (f . a) "\/" (f . b) by LATTICE3:44; :: thesis: verum

end;

for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b)

proof

let a, b be Element of L1; :: thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
A9: f . (a "/\" b) is_less_than {(f . a),(f . b)}

proof

( a "/\" b [= a & a "/\" b [= b ) by LATTICES:23;
then ( f . (a "/\" b) [= f . a & f . (a "/\" b) [= f . b ) by A2;
then for q being Element of L2 st q in {(f . a),(f . b)} holds
f . (a "/\" b) [= q by TARSKI:def 2;
hence f . (a "/\" b) is_less_than {(f . a),(f . b)} by LATTICE3:def 16; :: thesis: verum

end;

for r being Element of L2 st r is_less_than {(f . a),(f . b)} holds
r [= f . (a "/\" b)

proof

let r be Element of L2; :: thesis: ( r is_less_than {(f . a),(f . b)} implies r [= f . (a "/\" b) )
assume A10: r is_less_than {(f . a),(f . b)} ; :: thesis: r [= f . (a "/\" b)
( f . a in {(f . a),(f . b)} & f . b in {(f . a),(f . b)} ) by TARSKI:def 2;
then A11: ( r [= f . a & r [= f . b ) by A10, LATTICE3:def 16;
reconsider g = f " as Function of the carrier of L2,the carrier of L1 by A1, FUNCT_2:31;
A12: f . (g . r) = r by A1, FUNCT_1:57;
then ( g . r [= a & g . r [= b ) by A2, A11;
then for q being Element of L1 st q in {a,b} holds
g . r [= q by TARSKI:def 2;
then A13: g . r is_less_than {a,b} by LATTICE3:def 16;
a "/\" b = "/\" {a,b} by LATTICE3:44;
then g . r [= a "/\" b by A13, LATTICE3:34;
hence r [= f . (a "/\" b) by A2, A12; :: thesis: verum

end;

then f . (a "/\" b) = "/\" {(f . a),(f . b)},L2 by A9, LATTICE3:34;
hence f . (a "/\" b) = (f . a) "/\" (f . b) by LATTICE3:44; :: thesis: verum

end;

hence f is Homomorphism of L1,L2 by A3, LATTICE4:def 1; :: thesis: verum