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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 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:8; :: thesis: verum