consider z being Element of L2;
reconsider f = the carrier of L1 --> z 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) = z by FUNCOP_1:13
.= z "/\" z by YELLOW_5:2
.= (f . x) "/\" z by FUNCOP_1:13
.= (f . x) "/\" (f . y) by FUNCOP_1:13 ; :: 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) = z by FUNCOP_1:13
.= z "\/" z by YELLOW_5:1
.= (f . x) "\/" z by FUNCOP_1:13
.= (f . x) "\/" (f . y) by FUNCOP_1:13 ; :: thesis: verum

end;

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