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

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 Th16
.= (f . a) "\/" (f . b) by Def9 ; :: thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
thus f . (a "/\" b) = (f . a) /\ (f . b) by Th17
.= (f . a) "/\" (f . b) by Def10 ; :: thesis: verum

end;

hence StoneH L is Homomorphism of L, StoneLatt L by LATTICE4:def 1; :: thesis: verum