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;

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

hence
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
; :: thesis: verumlet 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;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