for G being Group
for A being Subgroup of G holds
( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )