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

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