set H = G;
take G ; :: thesis: ( G is Subgroup of G & ( for o being Element of O holds G ^ o = (G ^ o) | the carrier of G ) )

now

let o be Element of O; :: thesis: G ^ o = (G ^ o) | the carrier of G
set f = G ^ o;
dom (G ^ o) = the carrier of G by FUNCT_2:def 1;
hence G ^ o = (G ^ o) | the carrier of G by RELAT_1:98; :: thesis: verum

end;

hence ( G is Subgroup of G & ( for o being Element of O holds G ^ o = (G ^ o) | the carrier of G ) ) by GROUP_2:63; :: thesis: verum