let G be Group; :: thesis: for a, b being Element of G
for N being strict normal Subgroup of G st a in N holds
a |^ b in N
let a, b be Element of G; :: thesis: for N being strict normal Subgroup of G st a in N holds
a |^ b in N
let N be strict normal Subgroup of G; :: thesis: ( a in N implies a |^ b in N )
assume a in N ; :: thesis: a |^ b in N
then a |^ b in N |^ b by GROUP_3:58;
hence a |^ b in N by GROUP_3:def 13; :: thesis: verum