let L1, L2 be Lattice; :: thesis: for f being Function of the carrier of L1,the carrier of L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
let f be Function of the carrier of L1,the carrier of L2; :: thesis: ( f is onto implies for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 )
assume A1: f is onto ; :: thesis: for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
reconsider g = f as Function of the carrier of L1,the carrier of L2 ;
A2: rng g = the carrier of L2 by A1, FUNCT_2:def 3;

now

let a2 be Element of L2; :: thesis: ex a1 being Element of L1 st g . a1 = a2
consider x being set such that
A3: ( x in the carrier of L1 & g . x = a2 ) by A2, FUNCT_2:17;
thus ex a1 being Element of L1 st g . a1 = a2 by A3; :: thesis: verum

end;

hence for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 ; :: thesis: verum