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

A1: now

let x be Element of L1; :: thesis: ex b being Element of L2 st S₁[x,b]
take b = the Element of L2; :: 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) = the Element of L2 by A2
.= the Element of L2 "\/" the Element of L2 by LATTICES:1
.= (f . a1) "\/" the Element of L2 by A2
.= (f . a1) "\/" (f . b1) by A2 ; :: thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
thus f . (a1 "/\" b1) = the Element of L2 by A2
.= the Element of L2 "/\" the Element of L2 by LATTICES:2
.= (f . a1) "/\" the Element of L2 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