set z = the Element of L2;
reconsider f = the carrier of L1 --> the Element of L2 as Function of L1,L2 ;
take f ; :: thesis: ( f is meet-preserving & f is join-preserving )
for x, y being Element of L1 holds f . (x "/\" y) = (f . x) "/\" (f . y)

proof

let x, y be Element of L1; :: thesis: f . (x "/\" y) = (f . x) "/\" (f . y)
thus f . (x "/\" y) = the Element of L2 by FUNCOP_1:7
.= the Element of L2 "/\" the Element of L2 by YELLOW_5:2
.= (f . x) "/\" the Element of L2 by FUNCOP_1:7
.= (f . x) "/\" (f . y) by FUNCOP_1:7 ; :: thesis: verum

end;

hence f is meet-preserving by WAYBEL_6:1; :: thesis: f is join-preserving
for x, y being Element of L1 holds f . (x "\/" y) = (f . x) "\/" (f . y)

proof

let x, y be Element of L1; :: thesis: f . (x "\/" y) = (f . x) "\/" (f . y)
thus f . (x "\/" y) = the Element of L2 by FUNCOP_1:7
.= the Element of L2 "\/" the Element of L2 by YELLOW_5:1
.= (f . x) "\/" the Element of L2 by FUNCOP_1:7
.= (f . x) "\/" (f . y) by FUNCOP_1:7 ; :: thesis: verum

end;

hence f is join-preserving by WAYBEL_6:2; :: thesis: verum