consider b being Element of L2;
defpred S₁[ set , set ] means for a1 being Element of L1 st $1 = a1 holds
$2 = b;

A1: now

let x be Element of L1; :: thesis: ex b being Element of L2 st S₁[x,b]
take b = b; :: thesis: S₁[x,b]
thus S₁[x,b] ; :: thesis: verum

end;

consider f being Function of the carrier of L1, the carrier of L2 such that
A2: for x being Element of L1 holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for a1, b1 being Element of L1 holds
( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )

now

let a1, b1 be Element of L1; :: thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )
thus f . (a1 "\/" b1) = b by A2
.= b "\/" b by LATTICES:17
.= (f . a1) "\/" b by A2
.= (f . a1) "\/" (f . b1) by A2 ; :: thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
thus f . (a1 "/\" b1) = b by A2
.= b "/\" b by LATTICES:18
.= (f . a1) "/\" b by A2
.= (f . a1) "/\" (f . b1) by A2 ; :: thesis: verum

end;

hence for a1, b1 being Element of L1 holds
( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) ; :: thesis: verum