reconsider G' = HGrWOpStr(# the carrier of G,the multF of G,the action of G #) as strict StableSubgroup of G by Lm4;
consider H' being strict StableSubgroup of H such that
A1: the carrier of H' = g .: the carrier of G' by Lm17;
take H' ; :: thesis: the carrier of H' = g .: the carrier of G
thus the carrier of H' = g .: the carrier of G by A1; :: thesis: verum