let O be set ; :: thesis: for o being Element of O
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
(G ^ o) . g in H
let o be Element of O; :: thesis: for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
(G ^ o) . g in H
let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G
for g being Element of G st g in H holds
(G ^ o) . g in H
let H be StableSubgroup of G; :: thesis: for g being Element of G st g in H holds
(G ^ o) . g in H
let g be Element of G; :: thesis: ( g in H implies (G ^ o) . g in H )
set f = G ^ o;
assume g in H ; :: thesis: (G ^ o) . g in H
then A1: g in the carrier of H by STRUCT_0:def 5;
then (G ^ o) . g = ((G ^ o) | the carrier of H) . g by FUNCT_1:49;
then A2: (G ^ o) . g = (H ^ o) . g by Def7;
(H ^ o) . g in the carrier of H by A1, FUNCT_2:5;
hence (G ^ o) . g in H by A2, STRUCT_0:def 5; :: thesis: verum