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 )
reconsider g = f as Function of the carrier of L1, the carrier of L2 ;
assume f is onto ; :: thesis: for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
then A1: rng g = the carrier of L2 by FUNCT_2:def 3;

now

let a2 be Element of L2; :: thesis: ex a1 being Element of L1 st g . a1 = a2
ex x being set st
( x in the carrier of L1 & g . x = a2 ) by A1, FUNCT_2:11;
hence ex a1 being Element of L1 st g . a1 = a2 ; :: thesis: verum

end;

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