let L1, L2 be Lattice; :: thesis: for f being Function of the carrier of L1,the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
let f be Function of the carrier of L1,the carrier of L2; :: thesis: ( ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) implies f is one-to-one )
assume A1: for a, b being Element of L1 st f . a [= f . b holds
a [= b ; :: thesis: f is one-to-one
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in K41(f) or not y in K41(f) or not f . x = f . y or x = y )
assume that
A2: x in dom f and
A3: y in dom f and
A4: f . x = f . y ; :: thesis: x = y
reconsider y = y as Element of L1 by A3;
reconsider x = x as Element of L1 by A2;
( x [= y & y [= x ) by A1, A4;
hence x = y by LATTICES:26; :: thesis: verum