begin
definition
let G be
Group;
let N be
normal Subgroup of
G;
existence
ex b1 being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2
uniqueness
for b1, b2 being BinOp of (Cosets N) st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b2 . (W1,W2) = A1 * A2 ) holds
b1 = b2
end;
Lm1:
for G, H being Group
for a, b being Element of G
for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
Lm2:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
Lm3:
for H, G being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )