dom (StoneH L) = the carrier of L by Def6;
then reconsider f = StoneH L as Function of the carrier of L, the carrier of (StoneLatt L) by FUNCT_2:1;

now :: thesis: for a, b being Element of L holds
( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) )

let a, b be Element of L; :: thesis: ( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) )
thus f . (a "\/" b) = (f . a) \/ (f . b) by Th14
.= (f . a) "\/" (f . b) by Def9 ; :: thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
thus f . (a "/\" b) = (f . a) /\ (f . b) by Th15
.= (f . a) "/\" (f . b) by Def10 ; :: thesis: verum

end;

then ( f is "\/"-preserving & f is "/\"-preserving ) ;
hence StoneH L is Homomorphism of L,(StoneLatt L) ; :: thesis: verum