environ
vocabularies HIDDEN, XBOOLE_0, FUNCT_1, SUBSET_1, GROUP_1, GROUP_2, PRE_TOPC, RLSUB_1, NUMBERS, INT_1, STRUCT_0, RELAT_1, TARSKI, NEWTON, XXREAL_1, GROUP_4, GROUP_5, ALGSTR_0, NATTRA_1, ZFMISC_1, CARD_1, FINSET_1, BINOP_1, QC_LANG1, CQC_SIM1, REALSET1, MSSUBFAM, FUNCOP_1, ARYTM_3, XXREAL_0, COMPLEX1, FUNCT_2, WELLORD1, EQREL_1, GROUP_6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, BINOP_1, INT_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, NAT_1, GROUP_4, GROUP_5, INT_2;
definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, FUNCT_2;
theorems CARD_1, CARD_2, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_5, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_1, FUNCOP_1, NAT_1, ABSVALUE;
schemes BINOP_1, FUNCT_2, DOMAIN_1, NAT_1, CLASSES1;
registrations FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, ORDINAL1, RELSET_1;
constructors HIDDEN, RELAT_2, PARTFUN1, BINOP_1, FUNCOP_1, FINSUB_1, XXREAL_0, NAT_1, REAL_1, INT_2, REALSET2, GROUP_4, GROUP_5, RELSET_1, BINOP_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities XBOOLE_0, GROUP_2, BINOP_1, REALSET1, GROUP_4, ALGSTR_0, STRUCT_0, CARD_1, ORDINAL1;
expansions XBOOLE_0, GROUP_1, BINOP_1, FUNCT_2, STRUCT_0;
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 non empty unital multMagma
for f being Function of G,H st ( for a being Element of G holds f . a = 1_ H ) holds
for a, b being Element of G 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 G, H 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)) ) )