let L1, L2 be Lattice; :: thesis: for f being Function of L1,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 L1,L2; :: thesis: ( f is onto implies for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 )
assume f is onto ; :: thesis: for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
then A1: rng f = the carrier of L2 by FUNCT_2:def 3;
now :: thesis: for a2 being Element of L2 ex a1 being Element of L1 st f . a1 = a2
let a2 be Element of L2; :: thesis: ex a1 being Element of L1 st f . a1 = a2
ex x being object st
( x in the carrier of L1 & f . x = a2 ) by A1, FUNCT_2:11;
hence ex a1 being Element of L1 st f . a1 = a2 ; :: thesis: verum
end;
hence for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 ; :: thesis: verum