reconsider g = StoneH H as Function of the carrier of H,the carrier of (StoneLatt H) ;
set LH = Open_setLatt (HTopSpace H);
StoneS H c= the carrier of (Open_setLatt (HTopSpace H)) by Th37;
then reconsider f = g as Function of the carrier of H,the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:8;

now

let p', q' be Element of H; :: thesis: ( f . (p' "\/" q') = (f . p') "\/" (f . q') & f . (p' "/\" q') = (f . p') "/\" (f . q') )
thus f . (p' "\/" q') = ((StoneH H) . p') \/ ((StoneH H) . q') by Th16
.= (f . p') "\/" (f . q') by Def2 ; :: thesis: f . (p' "/\" q') = (f . p') "/\" (f . q')
thus f . (p' "/\" q') = ((StoneH H) . p') /\ ((StoneH H) . q') by Th17
.= (f . p') "/\" (f . q') by Def3 ; :: thesis: verum

end;

hence StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H) by LATTICE4:def 1; :: thesis: verum