:: deftheorem Def16 defines CosAc GROUP_9:def 16 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b₄ being Action of O,(Cosets N) holds
( ( not O is empty implies ( b₄ = CosAc N iff for o being Element of O holds b₄ . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } ) ) & ( O is empty implies ( b₄ = CosAc N iff b₄ = [:{},{(id (Cosets N))}:] ) ) );