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;

hence StoneH L is Homomorphism of L,(StoneLatt L) ; :: thesis: verum

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) )

then
( f is "\/"-preserving & f is "/\"-preserving )
;( 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;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

hence StoneH L is Homomorphism of L,(StoneLatt L) ; :: thesis: verum