let L be lower-bounded LATTICE; :: thesis: BasicDF L is onto
set X = the carrier of L;
set f = BasicDF L;
for w being object st w in the carrier of L holds
ex z being object st
( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )

proof

let w be object ; :: thesis: ( w in the carrier of L implies ex z being object st
( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z ) )
assume A1: w in the carrier of L ; :: thesis: ex z being object st
( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )
then reconsider w9 = w as Element of L ;
reconsider w99 = w as Element of L by A1;

per cases ( w = Bottom L or w <> Bottom L ) ;

suppose A2: w = Bottom L ; :: thesis: ex z being object st
( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )

reconsider z = [w,w] as set ;
take z ; :: thesis: ( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )
thus z in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; :: thesis: w = (BasicDF L) . z
thus (BasicDF L) . z = (BasicDF L) . (w9,w9)
.= w by A2, Def21 ; :: thesis: verum

end;

suppose A3: w <> Bottom L ; :: thesis: ex z being object st
( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )

reconsider z = [(Bottom L),w] as set ;
take z ; :: thesis: ( z in [: the carrier of L, the carrier of L:] & w = (BasicDF L) . z )
thus z in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; :: thesis: w = (BasicDF L) . z
thus (BasicDF L) . z = (BasicDF L) . ((Bottom L),w9)
.= (Bottom L) "\/" w99 by A3, Def21
.= w by WAYBEL_1:3 ; :: thesis: verum

end;

end;

end;

then rng (BasicDF L) = the carrier of L by FUNCT_2:10;
hence BasicDF L is onto by FUNCT_2:def 3; :: thesis: verum