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