let G be Group; :: thesis: for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let A be Subgroup of G; :: thesis: for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let a be Element of G; :: thesis: for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let X be Subgroup of A; :: thesis: for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let x be Element of A; :: thesis: ( x = a implies ( x * X = a * X & X * x = X * a ) )
set I = X;
assume A1: x = a ; :: thesis: ( x * X = a * X & X * x = X * a )
thus x * X c= a * X :: according to XBOOLE_0:def 10 :: thesis: ( a * X c= x * X & X * x = X * a )

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * X or y in a * X )
assume y in x * X ; :: thesis: y in a * X
then consider g being Element of A such that
A2: ( y = x * g & g in X ) by GROUP_2:103;
reconsider h = g as Element of G by GROUP_2:42;
a * h = x * g by A1, GROUP_2:43;
hence y in a * X by A2, GROUP_2:103; :: thesis: verum

end;

thus a * X c= x * X :: thesis: X * x = X * a

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in a * X or y in x * X )
assume y in a * X ; :: thesis: y in x * X
then consider b being Element of G such that
A3: y = a * b and
A4: b in X by GROUP_2:103;
reconsider c = b as Element of X by A4;
reconsider c = c as Element of A by GROUP_2:42;
a * b = x * c by A1, GROUP_2:43;
hence y in x * X by A3, A4, GROUP_2:103; :: thesis: verum

end;

thus X * x c= X * a :: according to XBOOLE_0:def 10 :: thesis: X * a c= X * x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X * x or y in X * a )
assume y in X * x ; :: thesis: y in X * a
then consider g being Element of A such that
A5: ( y = g * x & g in X ) by GROUP_2:104;
reconsider h = g as Element of G by GROUP_2:42;
h * a = g * x by A1, GROUP_2:43;
hence y in X * a by A5, GROUP_2:104; :: thesis: verum

end;

thus X * a c= X * x :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X * a or y in X * x )
assume y in X * a ; :: thesis: y in X * x
then consider b being Element of G such that
A6: y = b * a and
A7: b in X by GROUP_2:104;
reconsider c = b as Element of X by A7;
reconsider c = c as Element of A by GROUP_2:42;
b * a = c * x by A1, GROUP_2:43;
hence y in X * x by A6, A7, GROUP_2:104; :: thesis: verum

end;