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

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