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 set ; :: 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:125;
A4: Z " in A by A3, GROUP_2:60;
b " in (Omega). G by STRUCT_0:def 5;
then [.(b " ),(Z " ).] in [.((Omega). G),A.] by A4, GROUP_5:74;
then [.(b " ),(Z " ).] in A by A1, GROUP_2:49;
then A6: (((b * Z) * (b " )) * (Z " )) * Z in A by A3, GROUP_2:59;
A7: (((b * Z) * (b " )) * (Z " )) * Z = ((b * Z) * (b " )) * ((Z " ) * Z) by GROUP_1:def 4
.= ((b * Z) * (b " )) * (1_ G) by GROUP_1:def 6
.= (b * Z) * (b " ) by GROUP_1:def 5 ;
((b * Z) * (b " )) * b = (b * Z) * ((b " ) * b) by GROUP_1:def 4
.= (b * Z) * (1_ G) by GROUP_1:def 6
.= b * Z by GROUP_1:def 5 ;
hence x in A * b by A3, A6, A7, GROUP_2:126; :: thesis: verum

end;

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