let G be Group; :: thesis: for A being Subgroup of G holds
( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )
let A be Subgroup of G; :: thesis: ( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )
thus ( A is normal Subgroup of G implies [.A,((Omega). G).] is Subgroup of A ) by Lm3; :: thesis: ( [.A,((Omega). G).] is Subgroup of A implies A is normal Subgroup of G )
assume A1: [.A,((Omega). G).] is Subgroup of A ; :: thesis: A is normal Subgroup of G
for b being Element of G holds b * A c= A * b

proof

let b be Element of G; :: thesis: b * A c= A * b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in b * A or x in A * b )
assume A2: x in b * A ; :: thesis: x in A * b
then reconsider x = x as Element of G ;
consider Z being Element of G such that
A3: ( x = b * Z & Z in A ) by A2, GROUP_2:103;
A4: Z " in A by A3, GROUP_2:51;
b " in (Omega). G by STRUCT_0:def 5;
then [.(b "),(Z ").] in [.((Omega). G),A.] by A4, GROUP_5:65;
then [.(b "),(Z ").] in A by A1, GROUP_2:40;
then A5: (((b * Z) * (b ")) * (Z ")) * Z in A by A3, GROUP_2:50;
A6: (((b * Z) * (b ")) * (Z ")) * Z = ((b * Z) * (b ")) * ((Z ") * Z) by GROUP_1:def 3
.= ((b * Z) * (b ")) * (1_ G) by GROUP_1:def 5
.= (b * Z) * (b ") by GROUP_1:def 4 ;
((b * Z) * (b ")) * b = (b * Z) * ((b ") * b) by GROUP_1:def 3
.= (b * Z) * (1_ G) by GROUP_1:def 5
.= b * Z by GROUP_1:def 4 ;
hence x in A * b by A3, A5, A6, GROUP_2:104; :: thesis: verum

end;

hence A is normal Subgroup of G by GROUP_3:118; :: thesis: verum