:: GROUP_7 semantic presentation begin definition let R be Relation; attrR is multMagma-yielding means :Def1: :: GROUP_7:def 1 for y being set st y in rng R holds y is non empty multMagma ; end; :: deftheorem Def1 defines multMagma-yielding GROUP_7:def_1_:_ for R being Relation holds ( R is multMagma-yielding iff for y being set st y in rng R holds y is non empty multMagma ); registration cluster Relation-like Function-like multMagma-yielding -> 1-sorted-yielding for set ; coherence for b1 being Function st b1 is multMagma-yielding holds b1 is 1-sorted-yielding proof let f be Function; ::_thesis: ( f is multMagma-yielding implies f is 1-sorted-yielding ) assume A1: f is multMagma-yielding ; ::_thesis: f is 1-sorted-yielding let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom f or f . x is 1-sorted ) assume x in dom f ; ::_thesis: f . x is 1-sorted then f . x in rng f by FUNCT_1:def_3; hence f . x is 1-sorted by A1, Def1; ::_thesis: verum end; end; registration let I be set ; cluster Relation-like I -defined Function-like total multMagma-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is multMagma-yielding proof set H = the non empty multMagma ; set f = I --> the non empty multMagma ; take I --> the non empty multMagma ; ::_thesis: I --> the non empty multMagma is multMagma-yielding let a be set ; :: according to GROUP_7:def_1 ::_thesis: ( a in rng (I --> the non empty multMagma ) implies a is non empty multMagma ) assume a in rng (I --> the non empty multMagma ) ; ::_thesis: a is non empty multMagma then ex x being set st ( x in dom (I --> the non empty multMagma ) & a = (I --> the non empty multMagma ) . x ) by FUNCT_1:def_3; hence a is non empty multMagma by FUNCOP_1:7; ::_thesis: verum end; end; registration cluster Relation-like Function-like multMagma-yielding for set ; existence ex b1 being Function st b1 is multMagma-yielding proof set I = the set ; set f = the multMagma-yielding ManySortedSet of the set ; take the multMagma-yielding ManySortedSet of the set ; ::_thesis: the multMagma-yielding ManySortedSet of the set is multMagma-yielding thus the multMagma-yielding ManySortedSet of the set is multMagma-yielding ; ::_thesis: verum end; end; definition let I be set ; mode multMagma-Family of I is multMagma-yielding ManySortedSet of I; end; definition let I be non empty set ; let F be multMagma-Family of I; let i be Element of I; :: original: . redefine funcF . i -> non empty multMagma ; coherence F . i is non empty multMagma proof dom F = I by PARTFUN1:def_2; then F . i in rng F by FUNCT_1:def_3; hence F . i is non empty multMagma by Def1; ::_thesis: verum end; end; registration let I be set ; let F be multMagma-Family of I; cluster Carrier F -> V2() ; coherence Carrier F is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (Carrier F) . i is empty ) assume A1: i in I ; ::_thesis: not (Carrier F) . i is empty dom F = I by PARTFUN1:def_2; then F . i in rng F by A1, FUNCT_1:def_3; then A2: F . i is non empty multMagma by Def1; ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by A1, PRALG_1:def_13; hence not (Carrier F) . i is empty by A2; ::_thesis: verum end; end; Lm1: now__::_thesis:_for_I_being_non_empty_set_ for_i_being_Element_of_I for_F_being_multMagma-yielding_ManySortedSet_of_I for_f_being_Element_of_product_(Carrier_F)_holds_f_._i_in_the_carrier_of_(F_._i) let I be non empty set ; ::_thesis: for i being Element of I for F being multMagma-yielding ManySortedSet of I for f being Element of product (Carrier F) holds f . i in the carrier of (F . i) let i be Element of I; ::_thesis: for F being multMagma-yielding ManySortedSet of I for f being Element of product (Carrier F) holds f . i in the carrier of (F . i) let F be multMagma-yielding ManySortedSet of I; ::_thesis: for f being Element of product (Carrier F) holds f . i in the carrier of (F . i) let f be Element of product (Carrier F); ::_thesis: f . i in the carrier of (F . i) A1: dom (Carrier F) = I by PARTFUN1:def_2; ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; hence f . i in the carrier of (F . i) by A1, CARD_3:9; ::_thesis: verum end; definition let I be set ; let F be multMagma-Family of I; func product F -> strict multMagma means :Def2: :: GROUP_7:def 2 ( the carrier of it = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of it . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ); existence ex b1 being strict multMagma st ( the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) proof set A = product (Carrier F); defpred S1[ Element of product (Carrier F), Element of product (Carrier F), set ] means for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = \$3 & h . i = the multF of Fi . ((\$1 . i),(\$2 . i)) ); A1: dom (Carrier F) = I by PARTFUN1:def_2; A2: for x, y being Element of product (Carrier F) ex z being Element of product (Carrier F) st S1[x,y,z] proof let x, y be Element of product (Carrier F); ::_thesis: ex z being Element of product (Carrier F) st S1[x,y,z] defpred S2[ set , set ] means ex Fi being non empty multMagma st ( Fi = F . \$1 & \$2 = the multF of Fi . ((x . \$1),(y . \$1)) ); A3: for i being set st i in I holds ex w being set st ( w in union (rng (Carrier F)) & S2[i,w] ) proof let i be set ; ::_thesis: ( i in I implies ex w being set st ( w in union (rng (Carrier F)) & S2[i,w] ) ) assume A4: i in I ; ::_thesis: ex w being set st ( w in union (rng (Carrier F)) & S2[i,w] ) then reconsider I1 = I as non empty set ; reconsider i1 = i as Element of I1 by A4; reconsider F1 = F as multMagma-Family of I1 ; take w = the multF of (F1 . i1) . ((x . i1),(y . i1)); ::_thesis: ( w in union (rng (Carrier F)) & S2[i,w] ) A5: (Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def_3; A6: ex R being 1-sorted st ( R = F . i1 & (Carrier F1) . i1 = the carrier of R ) by PRALG_1:def_13; then A7: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9; x . i1 in the carrier of (F1 . i1) by A1, A6, CARD_3:9; then the multF of (F1 . i1) . ((x . i1),(y . i1)) in the carrier of (F1 . i1) by A7, BINOP_1:17; hence w in union (rng (Carrier F)) by A6, A5, TARSKI:def_4; ::_thesis: S2[i,w] thus S2[i,w] ; ::_thesis: verum end; consider z being Function such that A8: ( dom z = I & rng z c= union (rng (Carrier F)) & ( for x being set st x in I holds S2[x,z . x] ) ) from FUNCT_1:sch_5(A3); A9: for i being set st i in dom (Carrier F) holds z . i in (Carrier F) . i proof let i be set ; ::_thesis: ( i in dom (Carrier F) implies z . i in (Carrier F) . i ) assume A10: i in dom (Carrier F) ; ::_thesis: z . i in (Carrier F) . i then reconsider I1 = I as non empty set ; A11: ex Fi being non empty multMagma st ( Fi = F . i & z . i = the multF of Fi . ((x . i),(y . i)) ) by A8, A10; reconsider i1 = i as Element of I1 by A10; reconsider F1 = F as multMagma-Family of I1 ; A12: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by A10, PRALG_1:def_13; then A13: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9; x . i1 in the carrier of (F1 . i1) by A1, A12, CARD_3:9; hence z . i in (Carrier F) . i by A11, A12, A13, BINOP_1:17; ::_thesis: verum end; dom z = dom (Carrier F) by A8, PARTFUN1:def_2; then reconsider z = z as Element of product (Carrier F) by A9, CARD_3:9; take z ; ::_thesis: S1[x,y,z] let i be set ; ::_thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) ) assume i in I ; ::_thesis: ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) then consider Fi being non empty multMagma such that A14: Fi = F . i and A15: z . i = the multF of Fi . ((x . i),(y . i)) by A8; take Fi ; ::_thesis: ex h being Function st ( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) take z ; ::_thesis: ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) ) thus ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) ) by A14, A15; ::_thesis: verum end; consider B being BinOp of (product (Carrier F)) such that A16: for a, b being Element of product (Carrier F) holds S1[a,b,B . (a,b)] from BINOP_1:sch_3(A2); take multMagma(# (product (Carrier F)),B #) ; ::_thesis: ( the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) thus the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) ; ::_thesis: for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) let f, g be Element of product (Carrier F); ::_thesis: for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) let i be set ; ::_thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) assume i in I ; ::_thesis: ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) hence ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A16; ::_thesis: verum end; uniqueness for b1, b2 being strict multMagma st the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of b2 = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of b2 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) holds b1 = b2 proof let A, B be strict multMagma ; ::_thesis: ( the carrier of A = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of A . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of B = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of B . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) implies A = B ) assume that A17: the carrier of A = product (Carrier F) and A18: for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of A . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) and A19: the carrier of B = product (Carrier F) and A20: for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of B . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ; ::_thesis: A = B for x, y being set st x in the carrier of A & y in the carrier of A holds the multF of A . (x,y) = the multF of B . (x,y) proof set P = product (Carrier F); let x, y be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A implies the multF of A . (x,y) = the multF of B . (x,y) ) assume that A21: x in the carrier of A and A22: y in the carrier of A ; ::_thesis: the multF of A . (x,y) = the multF of B . (x,y) reconsider x1 = x, y1 = y as Element of product (Carrier F) by A17, A21, A22; [x1,y1] in [: the carrier of A, the carrier of A:] by A21, A22, ZFMISC_1:87; then reconsider f = the multF of A . [x1,y1] as Element of product (Carrier F) by A17, FUNCT_2:5; [x1,y1] in [: the carrier of B, the carrier of B:] by A19, ZFMISC_1:87; then reconsider g = the multF of B . [x1,y1] as Element of product (Carrier F) by A19, FUNCT_2:5; A23: dom (Carrier F) = I by PARTFUN1:def_2; then A24: dom g = I by CARD_3:9; A25: for i being set st i in I holds f . i = g . i proof let i be set ; ::_thesis: ( i in I implies f . i = g . i ) assume A26: i in I ; ::_thesis: f . i = g . i then A27: ex Gi being non empty multMagma ex h2 being Function st ( Gi = F . i & h2 = the multF of B . (x1,y1) & h2 . i = the multF of Gi . ((x1 . i),(y1 . i)) ) by A20; ex Fi being non empty multMagma ex h1 being Function st ( Fi = F . i & h1 = the multF of A . (x1,y1) & h1 . i = the multF of Fi . ((x1 . i),(y1 . i)) ) by A18, A26; hence f . i = g . i by A27; ::_thesis: verum end; dom f = I by A23, CARD_3:9; hence the multF of A . (x,y) = the multF of B . (x,y) by A24, A25, FUNCT_1:2; ::_thesis: verum end; hence A = B by A17, A19, BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def2 defines product GROUP_7:def_2_:_ for I being set for F being multMagma-Family of I for b3 being strict multMagma holds ( b3 = product F iff ( the carrier of b3 = product (Carrier F) & ( for f, g being Element of product (Carrier F) for i being set st i in I holds ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of b3 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) ); registration let I be set ; let F be multMagma-Family of I; cluster product F -> non empty strict constituted-Functions ; coherence ( not product F is empty & product F is constituted-Functions ) proof A1: the carrier of (product F) = product (Carrier F) by Def2; hence not the carrier of (product F) is empty ; :: according to STRUCT_0:def_1 ::_thesis: product F is constituted-Functions thus product F is constituted-Functions by A1, MONOID_0:80; ::_thesis: verum end; end; theorem Th4: :: GROUP_7:1 for I, i being set for f, g, h being Function for F being multMagma-Family of I for G being non empty multMagma for p, q being Element of (product F) for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i proof let I, i be set ; ::_thesis: for f, g, h being Function for F being multMagma-Family of I for G being non empty multMagma for p, q being Element of (product F) for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i let f, g, h be Function; ::_thesis: for F being multMagma-Family of I for G being non empty multMagma for p, q being Element of (product F) for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma for p, q being Element of (product F) for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i let G be non empty multMagma ; ::_thesis: for p, q being Element of (product F) for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i let p, q be Element of (product F); ::_thesis: for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds x * y = h . i let x, y be Element of G; ::_thesis: ( i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y implies x * y = h . i ) assume that A1: i in I and A2: G = F . i and A3: f = p and A4: g = q and A5: h = p * q and A6: f . i = x and A7: g . i = y ; ::_thesis: x * y = h . i set GP = product F; q in the carrier of (product F) ; then A8: g in product (Carrier F) by A4, Def2; p in the carrier of (product F) ; then f in product (Carrier F) by A3, Def2; then ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, Def2; hence x * y = h . i by A2, A3, A4, A5, A6, A7; ::_thesis: verum end; definition let I be set ; let F be multMagma-Family of I; attrF is Group-like means :Def3: :: GROUP_7:def 3 for i being set st i in I holds ex Fi being non empty Group-like multMagma st Fi = F . i; attrF is associative means :Def4: :: GROUP_7:def 4 for i being set st i in I holds ex Fi being non empty associative multMagma st Fi = F . i; attrF is commutative means :Def5: :: GROUP_7:def 5 for i being set st i in I holds ex Fi being non empty commutative multMagma st Fi = F . i; end; :: deftheorem Def3 defines Group-like GROUP_7:def_3_:_ for I being set for F being multMagma-Family of I holds ( F is Group-like iff for i being set st i in I holds ex Fi being non empty Group-like multMagma st Fi = F . i ); :: deftheorem Def4 defines associative GROUP_7:def_4_:_ for I being set for F being multMagma-Family of I holds ( F is associative iff for i being set st i in I holds ex Fi being non empty associative multMagma st Fi = F . i ); :: deftheorem Def5 defines commutative GROUP_7:def_5_:_ for I being set for F being multMagma-Family of I holds ( F is commutative iff for i being set st i in I holds ex Fi being non empty commutative multMagma st Fi = F . i ); definition let I be non empty set ; let F be multMagma-Family of I; redefine attr F is Group-like means :Def6: :: GROUP_7:def 6 for i being Element of I holds F . i is Group-like ; compatibility ( F is Group-like iff for i being Element of I holds F . i is Group-like ) proof hereby ::_thesis: ( ( for i being Element of I holds F . i is Group-like ) implies F is Group-like ) assume A1: F is Group-like ; ::_thesis: for i being Element of I holds F . i is Group-like let i be Element of I; ::_thesis: F . i is Group-like ex Fi being non empty Group-like multMagma st Fi = F . i by A1, Def3; hence F . i is Group-like ; ::_thesis: verum end; assume A2: for i being Element of I holds F . i is Group-like ; ::_thesis: F is Group-like let i be set ; :: according to GROUP_7:def_3 ::_thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = F . i ) assume i in I ; ::_thesis: ex Fi being non empty Group-like multMagma st Fi = F . i then reconsider i1 = i as Element of I ; reconsider F1 = F . i1 as non empty Group-like multMagma by A2; take F1 ; ::_thesis: F1 = F . i thus F1 = F . i ; ::_thesis: verum end; redefine attr F is associative means :Def7: :: GROUP_7:def 7 for i being Element of I holds F . i is associative ; compatibility ( F is associative iff for i being Element of I holds F . i is associative ) proof hereby ::_thesis: ( ( for i being Element of I holds F . i is associative ) implies F is associative ) assume A3: F is associative ; ::_thesis: for i being Element of I holds F . i is associative let i be Element of I; ::_thesis: F . i is associative ex Fi being non empty associative multMagma st Fi = F . i by A3, Def4; hence F . i is associative ; ::_thesis: verum end; assume A4: for i being Element of I holds F . i is associative ; ::_thesis: F is associative let i be set ; :: according to GROUP_7:def_4 ::_thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = F . i ) assume i in I ; ::_thesis: ex Fi being non empty associative multMagma st Fi = F . i then reconsider i1 = i as Element of I ; reconsider Fi = F . i1 as non empty associative multMagma by A4; take Fi ; ::_thesis: Fi = F . i thus Fi = F . i ; ::_thesis: verum end; redefine attr F is commutative means :: GROUP_7:def 8 for i being Element of I holds F . i is commutative ; compatibility ( F is commutative iff for i being Element of I holds F . i is commutative ) proof hereby ::_thesis: ( ( for i being Element of I holds F . i is commutative ) implies F is commutative ) assume A5: F is commutative ; ::_thesis: for i being Element of I holds F . i is commutative let i be Element of I; ::_thesis: F . i is commutative ex Fi being non empty commutative multMagma st Fi = F . i by A5, Def5; hence F . i is commutative ; ::_thesis: verum end; assume A6: for i being Element of I holds F . i is commutative ; ::_thesis: F is commutative let i be set ; :: according to GROUP_7:def_5 ::_thesis: ( i in I implies ex Fi being non empty commutative multMagma st Fi = F . i ) assume i in I ; ::_thesis: ex Fi being non empty commutative multMagma st Fi = F . i then reconsider i1 = i as Element of I ; reconsider Fi = F . i1 as non empty commutative multMagma by A6; take Fi ; ::_thesis: Fi = F . i thus Fi = F . i ; ::_thesis: verum end; end; :: deftheorem Def6 defines Group-like GROUP_7:def_6_:_ for I being non empty set for F being multMagma-Family of I holds ( F is Group-like iff for i being Element of I holds F . i is Group-like ); :: deftheorem Def7 defines associative GROUP_7:def_7_:_ for I being non empty set for F being multMagma-Family of I holds ( F is associative iff for i being Element of I holds F . i is associative ); :: deftheorem defines commutative GROUP_7:def_8_:_ for I being non empty set for F being multMagma-Family of I holds ( F is commutative iff for i being Element of I holds F . i is commutative ); registration let I be set ; cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative commutative for set ; existence ex b1 being multMagma-Family of I st ( b1 is Group-like & b1 is associative & b1 is commutative ) proof set H = the commutative Group; set f = I --> the commutative Group; I --> the commutative Group is multMagma-yielding proof let i be set ; :: according to GROUP_7:def_1 ::_thesis: ( i in rng (I --> the commutative Group) implies i is non empty multMagma ) assume i in rng (I --> the commutative Group) ; ::_thesis: i is non empty multMagma then ex x being set st ( x in dom (I --> the commutative Group) & i = (I --> the commutative Group) . x ) by FUNCT_1:def_3; hence i is non empty multMagma by FUNCOP_1:7; ::_thesis: verum end; then reconsider f = I --> the commutative Group as multMagma-Family of I ; take f ; ::_thesis: ( f is Group-like & f is associative & f is commutative ) hereby :: according to GROUP_7:def_3 ::_thesis: ( f is associative & f is commutative ) let i be set ; ::_thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = f . i ) assume A1: i in I ; ::_thesis: ex Fi being non empty Group-like multMagma st Fi = f . i then reconsider I1 = I as non empty set ; reconsider i1 = i as Element of I1 by A1; reconsider F1 = f as multMagma-Family of I1 ; reconsider Fi = F1 . i1 as non empty Group-like multMagma by FUNCOP_1:7; take Fi = Fi; ::_thesis: Fi = f . i thus Fi = f . i ; ::_thesis: verum end; hereby :: according to GROUP_7:def_4 ::_thesis: f is commutative let i be set ; ::_thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = f . i ) assume A2: i in I ; ::_thesis: ex Fi being non empty associative multMagma st Fi = f . i then reconsider I1 = I as non empty set ; reconsider i1 = i as Element of I1 by A2; reconsider F1 = f as multMagma-Family of I1 ; reconsider Fi = F1 . i1 as non empty associative multMagma by FUNCOP_1:7; take Fi = Fi; ::_thesis: Fi = f . i thus Fi = f . i ; ::_thesis: verum end; let i be set ; :: according to GROUP_7:def_5 ::_thesis: ( i in I implies ex Fi being non empty commutative multMagma st Fi = f . i ) assume A3: i in I ; ::_thesis: ex Fi being non empty commutative multMagma st Fi = f . i then reconsider I1 = I as non empty set ; reconsider i1 = i as Element of I1 by A3; reconsider F1 = f as multMagma-Family of I1 ; reconsider Fi = F1 . i1 as non empty commutative multMagma by FUNCOP_1:7; take Fi ; ::_thesis: Fi = f . i thus Fi = f . i ; ::_thesis: verum end; end; registration let I be set ; let F be Group-like multMagma-Family of I; cluster product F -> strict Group-like ; coherence product F is Group-like proof defpred S1[ set , set ] means ex Fi being non empty multMagma ex e being Element of Fi st ( Fi = F . I & F = e & ( for h being Element of Fi holds ( h * e = h & e * h = h & ex g being Element of Fi st ( h * g = e & g * h = e ) ) ) ); set G = product F; A1: dom (Carrier F) = I by PARTFUN1:def_2; A2: for i being set st i in I holds ex y being set st ( y in union (rng (Carrier F)) & S1[i,y] ) proof let i be set ; ::_thesis: ( i in I implies ex y being set st ( y in union (rng (Carrier F)) & S1[i,y] ) ) assume A3: i in I ; ::_thesis: ex y being set st ( y in union (rng (Carrier F)) & S1[i,y] ) then reconsider I1 = I as non empty set ; reconsider i1 = i as Element of I1 by A3; reconsider F1 = F as Group-like multMagma-Family of I1 ; A4: ex R being 1-sorted st ( R = F . i1 & (Carrier F1) . i1 = the carrier of R ) by PRALG_1:def_13; F1 . i1 is Group-like by Def6; then consider e being Element of (F1 . i1) such that A5: for h being Element of (F1 . i1) holds ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) by GROUP_1:def_2; take e ; ::_thesis: ( e in union (rng (Carrier F)) & S1[i,e] ) (Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def_3; hence e in union (rng (Carrier F)) by A4, TARSKI:def_4; ::_thesis: S1[i,e] take F1 . i1 ; ::_thesis: ex e being Element of (F1 . i1) st ( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) ) ) take e ; ::_thesis: ( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) ) ) thus ( F1 . i1 = F . i & e = e ) ; ::_thesis: for h being Element of (F1 . i1) holds ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) let h be Element of (F1 . i1); ::_thesis: ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) thus ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st ( h * g = e & g * h = e ) ) by A5; ::_thesis: verum end; consider ee being Function such that A6: dom ee = I and rng ee c= union (rng (Carrier F)) and A7: for x being set st x in I holds S1[x,ee . x] from FUNCT_1:sch_5(A2); now__::_thesis:_for_i_being_set_st_i_in_dom_ee_holds_ ee_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in dom ee implies ee . i in (Carrier F) . i ) assume A8: i in dom ee ; ::_thesis: ee . i in (Carrier F) . i then A9: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by A6, PRALG_1:def_13; ex Fi being non empty multMagma ex e being Element of Fi st ( Fi = F . i & ee . i = e & ( for h being Element of Fi holds ( h * e = h & e * h = h & ex g being Element of Fi st ( h * g = e & g * h = e ) ) ) ) by A6, A7, A8; hence ee . i in (Carrier F) . i by A9; ::_thesis: verum end; then A10: ee in product (Carrier F) by A1, A6, CARD_3:9; then reconsider e1 = ee as Element of (product F) by Def2; take e1 ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (product F) holds ( b1 * e1 = b1 & e1 * b1 = b1 & ex b2 being Element of the carrier of (product F) st ( b1 * b2 = e1 & b2 * b1 = e1 ) ) let h be Element of (product F); ::_thesis: ( h * e1 = h & e1 * h = h & ex b1 being Element of the carrier of (product F) st ( h * b1 = e1 & b1 * h = e1 ) ) reconsider h1 = h as Element of product (Carrier F) by Def2; reconsider he = the multF of (product F) . (h,e1), eh = the multF of (product F) . (e1,h) as Element of product (Carrier F) by Def2; A11: dom h1 = I by A1, CARD_3:9; A12: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ he_._i_=_h1_._i let i be set ; ::_thesis: ( i in I implies he . i = h1 . i ) assume A13: i in I ; ::_thesis: he . i = h1 . i then consider Fi being non empty multMagma , e2 being Element of Fi such that A14: Fi = F . i and A15: ee . i = e2 and A16: for h being Element of Fi holds ( h * e2 = h & e2 * h = h & ex g being Element of Fi st ( h * g = e2 & g * h = e2 ) ) by A7; reconsider h2 = h1 . i as Element of Fi by A13, A14, Lm1; A17: ex Gi being non empty multMagma ex f being Function st ( Gi = F . i & f = the multF of (product F) . (h1,e1) & f . i = the multF of Gi . ((h1 . i),(ee . i)) ) by A10, A13, Def2; h2 * e2 = h2 by A16; hence he . i = h1 . i by A17, A14, A15; ::_thesis: verum end; dom he = I by A1, CARD_3:9; hence h * e1 = h by A11, A12, FUNCT_1:2; ::_thesis: ( e1 * h = h & ex b1 being Element of the carrier of (product F) st ( h * b1 = e1 & b1 * h = e1 ) ) A18: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ eh_._i_=_h1_._i let i be set ; ::_thesis: ( i in I implies eh . i = h1 . i ) assume A19: i in I ; ::_thesis: eh . i = h1 . i then consider Fi being non empty multMagma , e2 being Element of Fi such that A20: Fi = F . i and A21: ee . i = e2 and A22: for h being Element of Fi holds ( h * e2 = h & e2 * h = h & ex g being Element of Fi st ( h * g = e2 & g * h = e2 ) ) by A7; reconsider h2 = h1 . i as Element of Fi by A19, A20, Lm1; A23: ex Gi being non empty multMagma ex f being Function st ( Gi = F . i & f = the multF of (product F) . (e1,h1) & f . i = the multF of Gi . ((ee . i),(h1 . i)) ) by A10, A19, Def2; e2 * h2 = h2 by A22; hence eh . i = h1 . i by A23, A20, A21; ::_thesis: verum end; defpred S2[ set , set ] means ex Fi being non empty multMagma ex hi being Element of Fi st ( Fi = F . I & hi = h1 . I & ex g being Element of Fi st ( hi * g = ee . I & g * hi = ee . I & F = g ) ); A24: for i being set st i in I holds ex y being set st ( y in union (rng (Carrier F)) & S2[i,y] ) proof let i be set ; ::_thesis: ( i in I implies ex y being set st ( y in union (rng (Carrier F)) & S2[i,y] ) ) assume A25: i in I ; ::_thesis: ex y being set st ( y in union (rng (Carrier F)) & S2[i,y] ) then consider Fi being non empty multMagma , e being Element of Fi such that A26: Fi = F . i and A27: ee . i = e and A28: for h being Element of Fi holds ( h * e = h & e * h = h & ex g being Element of Fi st ( h * g = e & g * h = e ) ) by A7; A29: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by A25, PRALG_1:def_13; reconsider hi = h1 . i as Element of Fi by A25, A26, Lm1; consider g being Element of Fi such that A30: hi * g = e and A31: g * hi = e by A28; take g ; ::_thesis: ( g in union (rng (Carrier F)) & S2[i,g] ) (Carrier F) . i in rng (Carrier F) by A1, A25, FUNCT_1:def_3; hence g in union (rng (Carrier F)) by A26, A29, TARSKI:def_4; ::_thesis: S2[i,g] take Fi ; ::_thesis: ex hi being Element of Fi st ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & g = g ) ) take hi ; ::_thesis: ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & g = g ) ) thus ( Fi = F . i & hi = h1 . i ) by A26; ::_thesis: ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & g = g ) take g ; ::_thesis: ( hi * g = ee . i & g * hi = ee . i & g = g ) thus ( hi * g = ee . i & g * hi = ee . i & g = g ) by A27, A30, A31; ::_thesis: verum end; consider gg being Function such that A32: dom gg = I and rng gg c= union (rng (Carrier F)) and A33: for x being set st x in I holds S2[x,gg . x] from FUNCT_1:sch_5(A24); now__::_thesis:_for_i_being_set_st_i_in_dom_gg_holds_ gg_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in dom gg implies gg . i in (Carrier F) . i ) assume A34: i in dom gg ; ::_thesis: gg . i in (Carrier F) . i then A35: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by A32, PRALG_1:def_13; ex Fi being non empty multMagma ex hi being Element of Fi st ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A32, A33, A34; hence gg . i in (Carrier F) . i by A35; ::_thesis: verum end; then A36: gg in product (Carrier F) by A1, A32, CARD_3:9; then reconsider g1 = gg as Element of (product F) by Def2; dom eh = I by A1, CARD_3:9; hence e1 * h = h by A11, A18, FUNCT_1:2; ::_thesis: ex b1 being Element of the carrier of (product F) st ( h * b1 = e1 & b1 * h = e1 ) take g1 ; ::_thesis: ( h * g1 = e1 & g1 * h = e1 ) reconsider he = the multF of (product F) . (h,g1), eh = the multF of (product F) . (g1,h) as Element of product (Carrier F) by Def2; A37: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ he_._i_=_ee_._i let i be set ; ::_thesis: ( i in I implies he . i = ee . i ) assume A38: i in I ; ::_thesis: he . i = ee . i then A39: ex Fi being non empty multMagma ex hi being Element of Fi st ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33; ex Gi being non empty multMagma ex h5 being Function st ( Gi = F . i & h5 = the multF of (product F) . (h1,gg) & h5 . i = the multF of Gi . ((h1 . i),(gg . i)) ) by A36, A38, Def2; hence he . i = ee . i by A39; ::_thesis: verum end; A40: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ eh_._i_=_ee_._i let i be set ; ::_thesis: ( i in I implies eh . i = ee . i ) assume A41: i in I ; ::_thesis: eh . i = ee . i then A42: ex Fi being non empty multMagma ex hi being Element of Fi st ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st ( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33; ex Gi being non empty multMagma ex h5 being Function st ( Gi = F . i & h5 = the multF of (product F) . (gg,h1) & h5 . i = the multF of Gi . ((gg . i),(h1 . i)) ) by A36, A41, Def2; hence eh . i = ee . i by A42; ::_thesis: verum end; dom he = I by A1, CARD_3:9; hence h * g1 = e1 by A6, A37, FUNCT_1:2; ::_thesis: g1 * h = e1 dom eh = I by A1, CARD_3:9; hence g1 * h = e1 by A6, A40, FUNCT_1:2; ::_thesis: verum end; end; registration let I be set ; let F be associative multMagma-Family of I; cluster product F -> strict associative ; coherence product F is associative proof set G = product F; let x, y, z be Element of (product F); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) reconsider x1 = x, y1 = y, z1 = z as Element of product (Carrier F) by Def2; set xy = the multF of (product F) . (x,y); set yz = the multF of (product F) . (y,z); set s = the multF of (product F) . (( the multF of (product F) . (x,y)),z); set t = the multF of (product F) . (x,( the multF of (product F) . (y,z))); reconsider xy = the multF of (product F) . (x,y), yz = the multF of (product F) . (y,z), s = the multF of (product F) . (( the multF of (product F) . (x,y)),z), t = the multF of (product F) . (x,( the multF of (product F) . (y,z))) as Element of product (Carrier F) by Def2; A1: dom (Carrier F) = I by PARTFUN1:def_2; then A2: dom t = I by CARD_3:9; A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ s_._i_=_t_._i let i be set ; ::_thesis: ( i in I implies s . i = t . i ) assume A4: i in I ; ::_thesis: s . i = t . i then consider XY being non empty multMagma , hxy being Function such that A5: XY = F . i and A6: hxy = the multF of (product F) . (x,y) and A7: hxy . i = the multF of XY . ((x1 . i),(y1 . i)) by Def2; A8: ex YZ being non empty multMagma ex hyz being Function st ( YZ = F . i & hyz = the multF of (product F) . (y,z) & hyz . i = the multF of YZ . ((y1 . i),(z1 . i)) ) by A4, Def2; reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1; consider XYZ1 being non empty multMagma , hxyz1 being Function such that A9: XYZ1 = F . i and A10: hxyz1 = the multF of (product F) . (xy,z) and A11: hxyz1 . i = the multF of XYZ1 . ((xy . i),(z1 . i)) by A4, Def2; reconsider zi = z1 . i, xiyi = xi * yi as Element of XYZ1 by A4, A5, A9, Lm1; reconsider xii = xi, yii = yi as Element of XYZ1 by A5, A9; A12: XYZ1 is associative by A4, A9, Def7; A13: ex XYZ2 being non empty multMagma ex hxyz2 being Function st ( XYZ2 = F . i & hxyz2 = the multF of (product F) . (x,yz) & hxyz2 . i = the multF of XYZ2 . ((x1 . i),(yz . i)) ) by A4, Def2; thus s . i = xiyi * zi by A6, A7, A10, A11 .= xii * (yii * zi) by A5, A9, A12, GROUP_1:def_3 .= t . i by A8, A9, A13 ; ::_thesis: verum end; dom s = I by A1, CARD_3:9; hence (x * y) * z = x * (y * z) by A2, A3, FUNCT_1:2; ::_thesis: verum end; end; registration let I be set ; let F be commutative multMagma-Family of I; cluster product F -> strict commutative ; coherence product F is commutative proof set G = product F; let x, y be Element of (product F); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x reconsider x1 = x, y1 = y, xy = the multF of (product F) . (x,y), yx = the multF of (product F) . (y,x) as Element of product (Carrier F) by Def2; A1: dom (Carrier F) = I by PARTFUN1:def_2; then A2: dom yx = I by CARD_3:9; A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ xy_._i_=_yx_._i let i be set ; ::_thesis: ( i in I implies xy . i = yx . i ) assume A4: i in I ; ::_thesis: xy . i = yx . i then consider XY being non empty multMagma , hxy being Function such that A5: XY = F . i and A6: hxy = the multF of (product F) . (x,y) and A7: hxy . i = the multF of XY . ((x1 . i),(y1 . i)) by Def2; reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1; A8: ex YX being non empty multMagma ex hyx being Function st ( YX = F . i & hyx = the multF of (product F) . (y,x) & hyx . i = the multF of YX . ((y1 . i),(x1 . i)) ) by A4, Def2; A9: ex Fi being non empty commutative multMagma st Fi = F . i by A4, Def5; thus xy . i = xi * yi by A6, A7 .= yi * xi by A5, A9, GROUP_1:def_12 .= yx . i by A5, A8 ; ::_thesis: verum end; dom xy = I by A1, CARD_3:9; hence x * y = y * x by A2, A3, FUNCT_1:2; ::_thesis: verum end; end; theorem :: GROUP_7:2 for I, i being set for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds G is Group-like proof let I, i be set ; ::_thesis: for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds G is Group-like let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds G is Group-like let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is Group-like implies G is Group-like ) assume that A1: i in I and A2: G = F . i ; ::_thesis: ( not product F is Group-like or G is Group-like ) set GP = product F; given e being Element of (product F) such that A3: for h being Element of (product F) holds ( h * e = h & e * h = h & ex g being Element of (product F) st ( h * g = e & g * h = e ) ) ; :: according to GROUP_1:def_2 ::_thesis: G is Group-like reconsider f = e as Element of product (Carrier F) by Def2; reconsider ei = f . i as Element of G by A1, A2, Lm1; take ei ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds ( b1 * ei = b1 & ei * b1 = b1 & ex b2 being Element of the carrier of G st ( b1 * b2 = ei & b2 * b1 = ei ) ) let h be Element of G; ::_thesis: ( h * ei = h & ei * h = h & ex b1 being Element of the carrier of G st ( h * b1 = ei & b1 * h = ei ) ) defpred S1[ set , set ] means ( ( \$1 = i implies \$2 = h ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A4: for j being set st j in I holds ex k being set st S1[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] ) assume A5: j in I ; ::_thesis: ex k being set st S1[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S1[j,k] hence ex k being set st S1[j,k] ; ::_thesis: verum end; supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k] j in dom F by A5, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S1[j, the Element of Fj] thus ( j = i implies the Element of Fj = h ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider g being ManySortedSet of I such that A7: for j being set st j in I holds S1[j,g . j] from PBOOLE:sch_3(A4); A8: dom g = I by PARTFUN1:def_2; A9: now__::_thesis:_for_j_being_set_st_j_in_dom_g_holds_ g_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom g implies g . b1 in (Carrier F) . b1 ) assume A10: j in dom g ; ::_thesis: g . b1 in (Carrier F) . b1 then A11: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA12: i = j ; ::_thesis: g . b1 in (Carrier F) . b1 then g . j = h by A7, A10; hence g . j in (Carrier F) . j by A2, A11, A12; ::_thesis: verum end; suppose j <> i ; ::_thesis: g . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & g . j = a ) by A7, A10; hence g . j in (Carrier F) . j by A11; ::_thesis: verum end; end; end; dom (Carrier F) = I by PARTFUN1:def_2; then reconsider g = g as Element of product (Carrier F) by A8, A9, CARD_3:9; A13: g . i = h by A1, A7; reconsider g1 = g as Element of (product F) by Def2; A14: e * g1 = g1 by A3; g1 * e = g1 by A3; hence ( h * ei = h & ei * h = h ) by A1, A2, A13, A14, Th4; ::_thesis: ex b1 being Element of the carrier of G st ( h * b1 = ei & b1 * h = ei ) consider gg being Element of (product F) such that A15: g1 * gg = e and A16: gg * g1 = e by A3; reconsider r = gg as Element of product (Carrier F) by Def2; reconsider r1 = r . i as Element of G by A1, A2, Lm1; take r1 ; ::_thesis: ( h * r1 = ei & r1 * h = ei ) thus ( h * r1 = ei & r1 * h = ei ) by A1, A2, A13, A15, A16, Th4; ::_thesis: verum end; theorem :: GROUP_7:3 for I, i being set for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is associative holds G is associative proof let I, i be set ; ::_thesis: for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is associative holds G is associative let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is associative holds G is associative let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is associative implies G is associative ) assume that A1: i in I and A2: G = F . i and A3: for x, y, z being Element of (product F) holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def_3 ::_thesis: G is associative let x, y, z be Element of G; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) defpred S1[ set , set ] means ( ( \$1 = i implies \$2 = y ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A4: for j being set st j in I holds ex k being set st S1[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] ) assume A5: j in I ; ::_thesis: ex k being set st S1[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S1[j,k] hence ex k being set st S1[j,k] ; ::_thesis: verum end; supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k] j in dom F by A5, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S1[j, the Element of Fj] thus ( j = i implies the Element of Fj = y ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider gy being ManySortedSet of I such that A7: for j being set st j in I holds S1[j,gy . j] from PBOOLE:sch_3(A4); A8: dom gy = I by PARTFUN1:def_2; A9: now__::_thesis:_for_j_being_set_st_j_in_dom_gy_holds_ gy_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom gy implies gy . b1 in (Carrier F) . b1 ) assume A10: j in dom gy ; ::_thesis: gy . b1 in (Carrier F) . b1 then A11: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA12: i = j ; ::_thesis: gy . b1 in (Carrier F) . b1 then gy . j = y by A7, A10; hence gy . j in (Carrier F) . j by A2, A11, A12; ::_thesis: verum end; suppose j <> i ; ::_thesis: gy . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & gy . j = a ) by A7, A10; hence gy . j in (Carrier F) . j by A11; ::_thesis: verum end; end; end; defpred S2[ set , set ] means ( ( \$1 = i implies \$2 = z ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A13: for j being set st j in I holds ex k being set st S2[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S2[j,k] ) assume A14: j in I ; ::_thesis: ex k being set st S2[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S2[j,k] hence ex k being set st S2[j,k] ; ::_thesis: verum end; supposeA15: j <> i ; ::_thesis: ex k being set st S2[j,k] j in dom F by A14, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S2[j, the Element of Fj] thus ( j = i implies the Element of Fj = z ) by A15; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider gz being ManySortedSet of I such that A16: for j being set st j in I holds S2[j,gz . j] from PBOOLE:sch_3(A13); set GP = product F; defpred S3[ set , set ] means ( ( \$1 = i implies \$2 = x ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A17: for j being set st j in I holds ex k being set st S3[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S3[j,k] ) assume A18: j in I ; ::_thesis: ex k being set st S3[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S3[j,k] hence ex k being set st S3[j,k] ; ::_thesis: verum end; supposeA19: j <> i ; ::_thesis: ex k being set st S3[j,k] j in dom F by A18, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S3[j, the Element of Fj] thus ( j = i implies the Element of Fj = x ) by A19; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider gx being ManySortedSet of I such that A20: for j being set st j in I holds S3[j,gx . j] from PBOOLE:sch_3(A17); A21: dom gx = I by PARTFUN1:def_2; A22: now__::_thesis:_for_j_being_set_st_j_in_dom_gx_holds_ gx_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom gx implies gx . b1 in (Carrier F) . b1 ) assume A23: j in dom gx ; ::_thesis: gx . b1 in (Carrier F) . b1 then A24: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA25: i = j ; ::_thesis: gx . b1 in (Carrier F) . b1 then gx . j = x by A20, A23; hence gx . j in (Carrier F) . j by A2, A24, A25; ::_thesis: verum end; suppose j <> i ; ::_thesis: gx . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & gx . j = a ) by A20, A23; hence gx . j in (Carrier F) . j by A24; ::_thesis: verum end; end; end; A26: dom gz = I by PARTFUN1:def_2; A27: now__::_thesis:_for_j_being_set_st_j_in_dom_gz_holds_ gz_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom gz implies gz . b1 in (Carrier F) . b1 ) assume A28: j in dom gz ; ::_thesis: gz . b1 in (Carrier F) . b1 then A29: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA30: i = j ; ::_thesis: gz . b1 in (Carrier F) . b1 then gz . j = z by A16, A28; hence gz . j in (Carrier F) . j by A2, A29, A30; ::_thesis: verum end; suppose j <> i ; ::_thesis: gz . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & gz . j = a ) by A16, A28; hence gz . j in (Carrier F) . j by A29; ::_thesis: verum end; end; end; A31: dom (Carrier F) = I by PARTFUN1:def_2; then reconsider gx = gx as Element of product (Carrier F) by A21, A22, CARD_3:9; reconsider gz = gz as Element of product (Carrier F) by A26, A31, A27, CARD_3:9; reconsider gy = gy as Element of product (Carrier F) by A8, A31, A9, CARD_3:9; reconsider x1 = gx, y1 = gy, z1 = gz as Element of (product F) by Def2; reconsider xy = x1 * y1, xyz3 = (x1 * y1) * z1, yz = y1 * z1, xyz5 = x1 * (y1 * z1) as Element of product (Carrier F) by Def2; reconsider xyi = xy . i, yzi = yz . i as Element of G by A1, A2, Lm1; A32: (x1 * y1) * z1 = x1 * (y1 * z1) by A3; A33: gx . i = x by A1, A20; then A34: x * yzi = xyz5 . i by A1, A2, Th4; A35: gz . i = z by A1, A16; then A36: xyi * z = xyz3 . i by A1, A2, Th4; A37: gy . i = y by A1, A7; then xy . i = x * y by A1, A2, A33, Th4; hence (x * y) * z = x * (y * z) by A1, A2, A32, A37, A35, A36, A34, Th4; ::_thesis: verum end; theorem :: GROUP_7:4 for I, i being set for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is commutative holds G is commutative proof let I, i be set ; ::_thesis: for F being multMagma-Family of I for G being non empty multMagma st i in I & G = F . i & product F is commutative holds G is commutative let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is commutative holds G is commutative let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is commutative implies G is commutative ) assume that A1: i in I and A2: G = F . i and A3: for x, y being Element of (product F) holds x * y = y * x ; :: according to GROUP_1:def_12 ::_thesis: G is commutative let x, y be Element of G; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x defpred S1[ set , set ] means ( ( \$1 = i implies \$2 = y ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A4: for j being set st j in I holds ex k being set st S1[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] ) assume A5: j in I ; ::_thesis: ex k being set st S1[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S1[j,k] hence ex k being set st S1[j,k] ; ::_thesis: verum end; supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k] j in dom F by A5, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S1[j, the Element of Fj] thus ( j = i implies the Element of Fj = y ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider gy being ManySortedSet of I such that A7: for j being set st j in I holds S1[j,gy . j] from PBOOLE:sch_3(A4); set GP = product F; defpred S2[ set , set ] means ( ( \$1 = i implies \$2 = x ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . \$1 & \$2 = a ) ) ); A8: for j being set st j in I holds ex k being set st S2[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S2[j,k] ) assume A9: j in I ; ::_thesis: ex k being set st S2[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S2[j,k] hence ex k being set st S2[j,k] ; ::_thesis: verum end; supposeA10: j <> i ; ::_thesis: ex k being set st S2[j,k] j in dom F by A9, PARTFUN1:def_2; then F . j in rng F by FUNCT_1:def_3; then reconsider Fj = F . j as non empty multMagma by Def1; set a = the Element of Fj; take the Element of Fj ; ::_thesis: S2[j, the Element of Fj] thus ( j = i implies the Element of Fj = x ) by A10; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st ( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum end; end; end; consider gx being ManySortedSet of I such that A11: for j being set st j in I holds S2[j,gx . j] from PBOOLE:sch_3(A8); A12: dom gy = I by PARTFUN1:def_2; A13: now__::_thesis:_for_j_being_set_st_j_in_dom_gy_holds_ gy_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom gy implies gy . b1 in (Carrier F) . b1 ) assume A14: j in dom gy ; ::_thesis: gy . b1 in (Carrier F) . b1 then A15: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA16: i = j ; ::_thesis: gy . b1 in (Carrier F) . b1 then gy . j = y by A7, A14; hence gy . j in (Carrier F) . j by A2, A15, A16; ::_thesis: verum end; suppose j <> i ; ::_thesis: gy . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & gy . j = a ) by A7, A14; hence gy . j in (Carrier F) . j by A15; ::_thesis: verum end; end; end; A17: dom (Carrier F) = I by PARTFUN1:def_2; then reconsider gy = gy as Element of product (Carrier F) by A12, A13, CARD_3:9; A18: gy . i = y by A1, A7; A19: dom gx = I by PARTFUN1:def_2; now__::_thesis:_for_j_being_set_st_j_in_dom_gx_holds_ gx_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom gx implies gx . b1 in (Carrier F) . b1 ) assume A20: j in dom gx ; ::_thesis: gx . b1 in (Carrier F) . b1 then A21: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA22: i = j ; ::_thesis: gx . b1 in (Carrier F) . b1 then gx . j = x by A11, A20; hence gx . j in (Carrier F) . j by A2, A21, A22; ::_thesis: verum end; suppose j <> i ; ::_thesis: gx . b1 in (Carrier F) . b1 then ex H being non empty multMagma ex a being Element of H st ( H = F . j & gx . j = a ) by A11, A20; hence gx . j in (Carrier F) . j by A21; ::_thesis: verum end; end; end; then reconsider gx = gx as Element of product (Carrier F) by A19, A17, CARD_3:9; reconsider x1 = gx, y1 = gy as Element of (product F) by Def2; A23: x1 * y1 = y1 * x1 by A3; reconsider xy = x1 * y1 as Element of product (Carrier F) by Def2; A24: gx . i = x by A1, A11; then xy . i = x * y by A1, A2, A18, Th4; hence x * y = y * x by A1, A2, A23, A24, A18, Th4; ::_thesis: verum end; theorem Th8: :: GROUP_7:5 for I being set for s being ManySortedSet of I for F being Group-like multMagma-Family of I st ( for i being set st i in I holds ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) ) holds s = 1_ (product F) proof let I be set ; ::_thesis: for s being ManySortedSet of I for F being Group-like multMagma-Family of I st ( for i being set st i in I holds ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) ) holds s = 1_ (product F) let s be ManySortedSet of I; ::_thesis: for F being Group-like multMagma-Family of I st ( for i being set st i in I holds ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) ) holds s = 1_ (product F) let F be Group-like multMagma-Family of I; ::_thesis: ( ( for i being set st i in I holds ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) ) implies s = 1_ (product F) ) assume A1: for i being set st i in I holds ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) ; ::_thesis: s = 1_ (product F) set GP = product F; A2: dom (Carrier F) = I by PARTFUN1:def_2; A3: dom s = I by PARTFUN1:def_2; now__::_thesis:_for_i_being_set_st_i_in_dom_s_holds_ s_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in dom s implies s . i in (Carrier F) . i ) assume A4: i in dom s ; ::_thesis: s . i in (Carrier F) . i then A5: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; ex G being non empty Group-like multMagma st ( G = F . i & s . i = 1_ G ) by A1, A4; hence s . i in (Carrier F) . i by A5; ::_thesis: verum end; then A6: s in product (Carrier F) by A3, A2, CARD_3:9; then reconsider e = s as Element of (product F) by Def2; now__::_thesis:_for_h_being_Element_of_(product_F)_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of (product F); ::_thesis: ( h * e = h & e * h = h ) reconsider h1 = h, he = h * e, eh = e * h as Element of product (Carrier F) by Def2; A7: dom h1 = I by A2, CARD_3:9; A8: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ he_._i_=_h1_._i let i be set ; ::_thesis: ( i in I implies he . i = h1 . i ) assume A9: i in I ; ::_thesis: he . i = h1 . i then consider G being non empty Group-like multMagma such that A10: G = F . i and A11: s . i = 1_ G by A1; reconsider b = h1 . i, c = s . i as Element of G by A9, A10, A11, Lm1; A12: ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (h,s) & m . i = the multF of Fi . ((h1 . i),(s . i)) ) by A6, A9, Def2; b * c = b by A11, GROUP_1:def_4; hence he . i = h1 . i by A12, A10; ::_thesis: verum end; dom he = I by A2, CARD_3:9; hence h * e = h by A7, A8, FUNCT_1:2; ::_thesis: e * h = h A13: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ eh_._i_=_h1_._i let i be set ; ::_thesis: ( i in I implies eh . i = h1 . i ) assume A14: i in I ; ::_thesis: eh . i = h1 . i then consider G being non empty Group-like multMagma such that A15: G = F . i and A16: s . i = 1_ G by A1; reconsider b = h1 . i, c = s . i as Element of G by A14, A15, A16, Lm1; A17: ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (s,h) & m . i = the multF of Fi . ((s . i),(h1 . i)) ) by A6, A14, Def2; c * b = b by A16, GROUP_1:def_4; hence eh . i = h1 . i by A17, A15; ::_thesis: verum end; dom eh = I by A2, CARD_3:9; hence e * h = h by A7, A13, FUNCT_1:2; ::_thesis: verum end; hence s = 1_ (product F) by GROUP_1:4; ::_thesis: verum end; theorem Th9: :: GROUP_7:6 for I, i being set for f being Function for F being Group-like multMagma-Family of I for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds f . i = 1_ G proof let I, i be set ; ::_thesis: for f being Function for F being Group-like multMagma-Family of I for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds f . i = 1_ G let f be Function; ::_thesis: for F being Group-like multMagma-Family of I for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds f . i = 1_ G let F be Group-like multMagma-Family of I; ::_thesis: for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds f . i = 1_ G let G be non empty Group-like multMagma ; ::_thesis: ( i in I & G = F . i & f = 1_ (product F) implies f . i = 1_ G ) assume that A1: i in I and A2: G = F . i and A3: f = 1_ (product F) ; ::_thesis: f . i = 1_ G set GP = product F; f in the carrier of (product F) by A3; then A4: f in product (Carrier F) by Def2; then reconsider e = f . i as Element of G by A1, A2, Lm1; now__::_thesis:_for_h_being_Element_of_G_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of G; ::_thesis: ( h * e = h & e * h = h ) defpred S1[ set , set ] means ( ( \$1 = i implies \$2 = h ) & ( \$1 <> i implies ex H being non empty Group-like multMagma st ( H = F . \$1 & \$2 = 1_ H ) ) ); A5: for j being set st j in I holds ex k being set st S1[j,k] proof let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] ) assume A6: j in I ; ::_thesis: ex k being set st S1[j,k] percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: ex k being set st S1[j,k] hence ex k being set st S1[j,k] ; ::_thesis: verum end; supposeA7: j <> i ; ::_thesis: ex k being set st S1[j,k] consider Fj being non empty Group-like multMagma such that A8: Fj = F . j by A6, Def3; take 1_ Fj ; ::_thesis: S1[j, 1_ Fj] thus ( j = i implies 1_ Fj = h ) by A7; ::_thesis: ( j <> i implies ex H being non empty Group-like multMagma st ( H = F . j & 1_ Fj = 1_ H ) ) thus ( j <> i implies ex H being non empty Group-like multMagma st ( H = F . j & 1_ Fj = 1_ H ) ) by A8; ::_thesis: verum end; end; end; consider g being ManySortedSet of I such that A9: for j being set st j in I holds S1[j,g . j] from PBOOLE:sch_3(A5); A10: dom g = I by PARTFUN1:def_2; A11: now__::_thesis:_for_j_being_set_st_j_in_dom_g_holds_ g_._j_in_(Carrier_F)_._j let j be set ; ::_thesis: ( j in dom g implies g . b1 in (Carrier F) . b1 ) assume A12: j in dom g ; ::_thesis: g . b1 in (Carrier F) . b1 then A13: ex R being 1-sorted st ( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13; percases ( i = j or j <> i ) ; supposeA14: i = j ; ::_thesis: g . b1 in (Carrier F) . b1 then g . j = h by A9, A12; hence g . j in (Carrier F) . j by A2, A13, A14; ::_thesis: verum end; suppose j <> i ; ::_thesis: g . b1 in (Carrier F) . b1 then ex H being non empty Group-like multMagma st ( H = F . j & g . j = 1_ H ) by A9, A12; hence g . j in (Carrier F) . j by A13; ::_thesis: verum end; end; end; dom (Carrier F) = I by PARTFUN1:def_2; then A15: g in product (Carrier F) by A10, A11, CARD_3:9; then reconsider g1 = g as Element of (product F) by Def2; A16: g1 * (1_ (product F)) = g1 by GROUP_1:def_4; A17: g . i = h by A1, A9; A18: g . i = h by A1, A9; ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (g,f) & m . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A4, A15, Def2; hence h * e = h by A2, A3, A16, A18; ::_thesis: e * h = h A19: (1_ (product F)) * g1 = g1 by GROUP_1:def_4; ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A4, A15, Def2; hence e * h = h by A2, A3, A19, A17; ::_thesis: verum end; hence f . i = 1_ G by GROUP_1:4; ::_thesis: verum end; theorem Th10: :: GROUP_7:7 for I being set for g being Function for s being ManySortedSet of I for F being Group-like associative multMagma-Family of I for x being Element of (product F) st x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) holds s = x " proof let I be set ; ::_thesis: for g being Function for s being ManySortedSet of I for F being Group-like associative multMagma-Family of I for x being Element of (product F) st x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) holds s = x " let g be Function; ::_thesis: for s being ManySortedSet of I for F being Group-like associative multMagma-Family of I for x being Element of (product F) st x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) holds s = x " let s be ManySortedSet of I; ::_thesis: for F being Group-like associative multMagma-Family of I for x being Element of (product F) st x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) holds s = x " let F be Group-like associative multMagma-Family of I; ::_thesis: for x being Element of (product F) st x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) holds s = x " let x be Element of (product F); ::_thesis: ( x = g & ( for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ) implies s = x " ) assume that A1: x = g and A2: for i being set st i in I holds ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) ; ::_thesis: s = x " set GP = product F; A3: dom (Carrier F) = I by PARTFUN1:def_2; A4: dom s = I by PARTFUN1:def_2; now__::_thesis:_for_i_being_set_st_i_in_dom_s_holds_ s_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in dom s implies s . i in (Carrier F) . i ) assume A5: i in dom s ; ::_thesis: s . i in (Carrier F) . i then A6: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; ex G being Group ex y being Element of G st ( G = F . i & s . i = y " & y = g . i ) by A2, A5; hence s . i in (Carrier F) . i by A6; ::_thesis: verum end; then A7: s in product (Carrier F) by A3, A4, CARD_3:9; then reconsider f1 = s as Element of (product F) by Def2; reconsider II = 1_ (product F), xf = x * f1, fx = f1 * x, x1 = x as Element of product (Carrier F) by Def2; A8: dom II = I by A3, CARD_3:9; A9: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ fx_._i_=_II_._i let i be set ; ::_thesis: ( i in I implies fx . i = II . i ) assume A10: i in I ; ::_thesis: fx . i = II . i then consider G being Group, y being Element of G such that A11: G = F . i and A12: s . i = y " and A13: y = g . i by A2; A14: ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (s,x) & m . i = the multF of Fi . ((s . i),(x1 . i)) ) by A7, A10, Def2; (y ") * y = 1_ G by GROUP_1:def_5; hence fx . i = II . i by A1, A10, A14, A11, A12, A13, Th9; ::_thesis: verum end; dom fx = I by A3, CARD_3:9; then A15: f1 * x = 1_ (product F) by A8, A9, FUNCT_1:2; A16: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ xf_._i_=_II_._i let i be set ; ::_thesis: ( i in I implies xf . i = II . i ) assume A17: i in I ; ::_thesis: xf . i = II . i then consider G being Group, y being Element of G such that A18: G = F . i and A19: s . i = y " and A20: y = g . i by A2; A21: ex Fi being non empty multMagma ex m being Function st ( Fi = F . i & m = the multF of (product F) . (x,s) & m . i = the multF of Fi . ((x1 . i),(s . i)) ) by A7, A17, Def2; y * (y ") = 1_ G by GROUP_1:def_5; hence xf . i = II . i by A1, A17, A21, A18, A19, A20, Th9; ::_thesis: verum end; dom xf = I by A3, CARD_3:9; then x * f1 = 1_ (product F) by A8, A16, FUNCT_1:2; hence s = x " by A15, GROUP_1:def_5; ::_thesis: verum end; theorem Th11: :: GROUP_7:8 for I, i being set for f, g being Function for F being Group-like associative multMagma-Family of I for x being Element of (product F) for G being Group for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " proof let I, i be set ; ::_thesis: for f, g being Function for F being Group-like associative multMagma-Family of I for x being Element of (product F) for G being Group for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " let f, g be Function; ::_thesis: for F being Group-like associative multMagma-Family of I for x being Element of (product F) for G being Group for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " let F be Group-like associative multMagma-Family of I; ::_thesis: for x being Element of (product F) for G being Group for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " let x be Element of (product F); ::_thesis: for G being Group for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " let G be Group; ::_thesis: for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds g . i = y " let y be Element of G; ::_thesis: ( i in I & G = F . i & f = x & g = x " & f . i = y implies g . i = y " ) assume that A1: i in I and A2: G = F . i and A3: f = x and A4: g = x " and A5: f . i = y ; ::_thesis: g . i = y " set GP = product F; A6: the multF of (product F) . (g,f) = (x ") * x by A3, A4 .= 1_ (product F) by GROUP_1:def_5 ; x " in the carrier of (product F) ; then A7: g in product (Carrier F) by A4, Def2; then reconsider gi = g . i as Element of G by A1, A2, Lm1; x in the carrier of (product F) ; then A8: f in product (Carrier F) by A3, Def2; then ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of (product F) . (g,f) & h . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A7, Def2; then A9: gi * y = 1_ G by A1, A2, A5, A6, Th9; A10: the multF of (product F) . (f,g) = x * (x ") by A3, A4 .= 1_ (product F) by GROUP_1:def_5 ; ex Fi being non empty multMagma ex h being Function st ( Fi = F . i & h = the multF of (product F) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, A7, Def2; then y * gi = 1_ G by A1, A2, A5, A10, Th9; hence g . i = y " by A9, GROUP_1:def_5; ::_thesis: verum end; definition let I be set ; let F be Group-like associative multMagma-Family of I; func sum F -> strict Subgroup of product F means :Def9: :: GROUP_7:def 9 for x being set holds ( x in the carrier of it iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ); existence ex b1 being strict Subgroup of product F st for x being set holds ( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) proof set GP = product F; set CF = Carrier F; A1: dom (Carrier F) = I by PARTFUN1:def_2; reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2; A2: dom g = dom (Carrier F) by CARD_3:9; defpred S1[ set ] means ex J being finite Subset of I ex f being ManySortedSet of J st ( \$1 = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ); consider A being set such that A3: for x being set holds ( x in A iff ( x in product (Carrier F) & S1[x] ) ) from XBOOLE_0:sch_1(); A4: A c= the carrier of (product F) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in the carrier of (product F) ) assume a in A ; ::_thesis: a in the carrier of (product F) then a in product (Carrier F) by A3; hence a in the carrier of (product F) by Def2; ::_thesis: verum end; A5: S1[g] proof set J = {} I; dom {} = {} I ; then reconsider f = {} as ManySortedSet of {} I by PARTFUN1:def_2, RELAT_1:def_18; take {} I ; ::_thesis: ex f being ManySortedSet of {} I st ( g = g +* f & ( for j being set st j in {} I holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) take f ; ::_thesis: ( g = g +* f & ( for j being set st j in {} I holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) thus g = g +* {} .= g +* f ; ::_thesis: for j being set st j in {} I holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) thus for j being set st j in {} I holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; ::_thesis: verum end; then reconsider A = A as non empty set by A3; set b = the multF of (product F) || A; A6: for p being Element of product (Carrier F) holds dom p = I by PARTFUN1:def_2; ( dom ( the multF of (product F) || A) = [:A,A:] & rng ( the multF of (product F) || A) c= A ) proof dom the multF of (product F) = [: the carrier of (product F), the carrier of (product F):] by FUNCT_2:def_1; hence A7: dom ( the multF of (product F) || A) = [:A,A:] by A4, RELAT_1:62, ZFMISC_1:96; ::_thesis: rng ( the multF of (product F) || A) c= A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the multF of (product F) || A) or y in A ) assume y in rng ( the multF of (product F) || A) ; ::_thesis: y in A then consider x being set such that A8: x in dom ( the multF of (product F) || A) and A9: ( the multF of (product F) || A) . x = y by FUNCT_1:def_3; consider x1, x2 being set such that A10: x1 in A and A11: x2 in A and A12: x = [x1,x2] by A7, A8, ZFMISC_1:def_2; consider J1 being finite Subset of I, f1 being ManySortedSet of J1 such that A13: x1 = g +* f1 and A14: for j being set st j in J1 holds ex G being non empty Group-like multMagma st ( G = F . j & f1 . j in the carrier of G & f1 . j <> 1_ G ) by A3, A10; consider J2 being finite Subset of I, f2 being ManySortedSet of J2 such that A15: x2 = g +* f2 and A16: for j being set st j in J2 holds ex G being non empty Group-like multMagma st ( G = F . j & f2 . j in the carrier of G & f2 . j <> 1_ G ) by A3, A11; reconsider x1 = x1, x2 = x2 as Function by A13, A15; A17: dom f1 = J1 by PARTFUN1:def_2; A18: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x1_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in I implies x1 . b1 in (Carrier F) . b1 ) assume A19: i in I ; ::_thesis: x1 . b1 in (Carrier F) . b1 then A20: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; percases ( i in J1 or not i in J1 ) ; supposeA21: i in J1 ; ::_thesis: x1 . b1 in (Carrier F) . b1 then ex G being non empty Group-like multMagma st ( G = F . i & f1 . i in the carrier of G & f1 . i <> 1_ G ) by A14; hence x1 . i in (Carrier F) . i by A13, A17, A20, A21, FUNCT_4:13; ::_thesis: verum end; supposeA22: not i in J1 ; ::_thesis: x1 . b1 in (Carrier F) . b1 consider G being non empty Group-like multMagma such that A23: G = F . i by A19, Def3; x1 . i = g . i by A13, A17, A22, FUNCT_4:11 .= 1_ G by A19, A23, Th9 ; hence x1 . i in (Carrier F) . i by A20, A23; ::_thesis: verum end; end; end; A24: dom f2 = J2 by PARTFUN1:def_2; A25: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ x2_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in I implies x2 . b1 in (Carrier F) . b1 ) assume A26: i in I ; ::_thesis: x2 . b1 in (Carrier F) . b1 then A27: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; percases ( i in J2 or not i in J2 ) ; supposeA28: i in J2 ; ::_thesis: x2 . b1 in (Carrier F) . b1 then ex G being non empty Group-like multMagma st ( G = F . i & f2 . i in the carrier of G & f2 . i <> 1_ G ) by A16; hence x2 . i in (Carrier F) . i by A15, A24, A27, A28, FUNCT_4:13; ::_thesis: verum end; supposeA29: not i in J2 ; ::_thesis: x2 . b1 in (Carrier F) . b1 consider G being non empty Group-like multMagma such that A30: G = F . i by A26, Def3; x2 . i = g . i by A15, A24, A29, FUNCT_4:11 .= 1_ G by A26, A30, Th9 ; hence x2 . i in (Carrier F) . i by A27, A30; ::_thesis: verum end; end; end; A31: dom x1 = (dom g) \/ (dom f1) by A13, FUNCT_4:def_1 .= I by A2, A1, A17, XBOOLE_1:12 ; dom x2 = (dom g) \/ (dom f2) by A15, FUNCT_4:def_1 .= I by A2, A1, A24, XBOOLE_1:12 ; then reconsider x2 = x2 as Element of product (Carrier F) by A1, A25, CARD_3:9; reconsider x1 = x1 as Element of product (Carrier F) by A1, A31, A18, CARD_3:9; reconsider X1 = x1, X2 = x2 as Element of (product F) by Def2; A32: [x1,x2] in [:A,A:] by A10, A11, ZFMISC_1:87; then A33: y = X1 * X2 by A9, A12, FUNCT_1:49; then reconsider y1 = y as Element of product (Carrier F) by Def2; defpred S2[ set ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st ( G = F . \$1 & k1 = x1 . \$1 & k2 = x2 . \$1 & k1 * k2 = 1_ G & f1 . \$1 <> 1_ G & f2 . \$1 <> 1_ G ); consider K being set such that A34: for k being set holds ( k in K iff ( k in I & S2[k] ) ) from XBOOLE_0:sch_1(); A35: S1[y] proof defpred S3[ set , set ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st ( G = F . \$1 & k1 = x1 . \$1 & k2 = x2 . \$1 & \$2 = k1 * k2 ); reconsider J = (J1 \/ J2) \ K as finite Subset of I ; take J ; ::_thesis: ex f being ManySortedSet of J st ( y = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) A36: dom y1 = I by A6; A37: for j being set st j in J holds ex t being set st S3[j,t] proof let j be set ; ::_thesis: ( j in J implies ex t being set st S3[j,t] ) assume A38: j in J ; ::_thesis: ex t being set st S3[j,t] then consider G being non empty Group-like multMagma such that A39: G = F . j by Def3; reconsider k1 = x1 . j, k2 = x2 . j as Element of G by A38, A39, Lm1; take k1 * k2 ; ::_thesis: S3[j,k1 * k2] thus S3[j,k1 * k2] by A39; ::_thesis: verum end; consider f being ManySortedSet of J such that A40: for j being set st j in J holds S3[j,f . j] from PBOOLE:sch_3(A37); take f ; ::_thesis: ( y = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) set gf = g +* f; A41: dom f = J by PARTFUN1:def_2; A42: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ y1_._i_=_(g_+*_f)_._i let i be set ; ::_thesis: ( i in I implies y1 . b1 = (g +* f) . b1 ) assume A43: i in I ; ::_thesis: y1 . b1 = (g +* f) . b1 then consider Fi being non empty multMagma , h being Function such that A44: Fi = F . i and A45: h = the multF of (product F) . (x1,x2) and A46: h . i = the multF of Fi . ((x1 . i),(x2 . i)) by Def2; consider FF being non empty Group-like multMagma such that A47: FF = F . i by A43, Def3; reconsider Fi = Fi as non empty Group-like multMagma by A44, A47; reconsider x1i = x1 . i, x2i = x2 . i as Element of Fi by A43, A44, Lm1; A48: y1 . i = x1i * x2i by A9, A12, A32, A45, A46, FUNCT_1:49; percases ( i in J or not i in J ) ; supposeA49: i in J ; ::_thesis: y1 . b1 = (g +* f) . b1 then ex GG being non empty Group-like multMagma ex k1a, k2a being Element of GG st ( GG = F . i & k1a = x1 . i & k2a = x2 . i & f . i = k1a * k2a ) by A40; hence y1 . i = (g +* f) . i by A33, A41, A44, A45, A46, A49, FUNCT_4:13; ::_thesis: verum end; supposeA50: not i in J ; ::_thesis: y1 . b1 = (g +* f) . b1 then A51: (g +* f) . i = g . i by A41, FUNCT_4:11 .= 1_ FF by A43, A47, Th9 ; now__::_thesis:_(_(_not_i_in_J1_\/_J2_&_y1_._i_=_(g_+*_f)_._i_)_or_(_i_in_K_&_y1_._i_=_(g_+*_f)_._i_)_) percases ( not i in J1 \/ J2 or i in K ) by A50, XBOOLE_0:def_5; caseA52: not i in J1 \/ J2 ; ::_thesis: y1 . i = (g +* f) . i then not i in J2 by XBOOLE_0:def_3; then x2 . i = g . i by A15, A24, FUNCT_4:11; then A53: x2 . i = 1_ FF by A43, A47, Th9; not i in J1 by A52, XBOOLE_0:def_3; then x1 . i = g . i by A13, A17, FUNCT_4:11; then x1 . i = 1_ FF by A43, A47, Th9; hence y1 . i = (g +* f) . i by A44, A47, A48, A51, A53, GROUP_1:def_4; ::_thesis: verum end; case i in K ; ::_thesis: y1 . i = (g +* f) . i then ex GG being non empty Group-like multMagma ex k1, k2 being Element of GG st ( GG = F . i & k1 = x1 . i & k2 = x2 . i & k1 * k2 = 1_ GG & f1 . i <> 1_ GG & f2 . i <> 1_ GG ) by A34; hence y1 . i = (g +* f) . i by A33, A43, A47, A51, Th4; ::_thesis: verum end; end; end; hence y1 . i = (g +* f) . i ; ::_thesis: verum end; end; end; dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1 .= I by A2, A1, A41, XBOOLE_1:12 ; hence y = g +* f by A36, A42, FUNCT_1:2; ::_thesis: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) assume A54: j in J ; ::_thesis: ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) then consider G being non empty Group-like multMagma , k1, k2 being Element of G such that A55: G = F . j and A56: k1 = x1 . j and A57: k2 = x2 . j and A58: f . j = k1 * k2 by A40; take G ; ::_thesis: ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) thus G = F . j by A55; ::_thesis: ( f . j in the carrier of G & f . j <> 1_ G ) thus f . j in the carrier of G by A58; ::_thesis: f . j <> 1_ G A59: j in J1 \/ J2 by A54, XBOOLE_0:def_5; percases ( ( j in J1 & not j in J2 ) or ( not j in J1 & j in J2 ) or ( j in J1 & j in J2 ) ) by A59, XBOOLE_0:def_3; supposeA60: ( j in J1 & not j in J2 ) ; ::_thesis: f . j <> 1_ G then A61: x1 . j = f1 . j by A13, A17, FUNCT_4:13; consider G1 being non empty Group-like multMagma such that A62: G1 = F . j and f1 . j in the carrier of G1 and A63: f1 . j <> 1_ G1 by A14, A60; x2 . j = g . j by A15, A24, A60, FUNCT_4:11 .= 1_ G1 by A54, A62, Th9 ; hence f . j <> 1_ G by A55, A56, A57, A58, A61, A62, A63, GROUP_1:def_4; ::_thesis: verum end; supposeA64: ( not j in J1 & j in J2 ) ; ::_thesis: f . j <> 1_ G then A65: x2 . j = f2 . j by A15, A24, FUNCT_4:13; consider G2 being non empty Group-like multMagma such that A66: G2 = F . j and f2 . j in the carrier of G2 and A67: f2 . j <> 1_ G2 by A16, A64; x1 . j = g . j by A13, A17, A64, FUNCT_4:11 .= 1_ G2 by A54, A66, Th9 ; hence f . j <> 1_ G by A55, A56, A57, A58, A65, A66, A67, GROUP_1:def_4; ::_thesis: verum end; supposeA68: ( j in J1 & j in J2 ) ; ::_thesis: f . j <> 1_ G then A69: ex G2 being non empty Group-like multMagma st ( G2 = F . j & f2 . j in the carrier of G2 & f2 . j <> 1_ G2 ) by A16; A70: not j in K by A54, XBOOLE_0:def_5; ex G1 being non empty Group-like multMagma st ( G1 = F . j & f1 . j in the carrier of G1 & f1 . j <> 1_ G1 ) by A14, A68; hence f . j <> 1_ G by A34, A54, A55, A56, A57, A58, A69, A70; ::_thesis: verum end; end; end; reconsider ff = X1 * X2 as Element of product (Carrier F) by Def2; now__::_thesis:_ex_J_being_finite_Subset_of_I_st_ for_j_being_set_st_j_in_J_holds_ ex_G_being_non_empty_Group-like_multMagma_st_ (_G_=_F_._j_&_ff_._j_in_the_carrier_of_G_&_ff_._j_<>_1__G_) reconsider J = {} as finite Subset of I by XBOOLE_1:2; take J = J; ::_thesis: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) thus for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ; ::_thesis: verum end; hence y in A by A3, A33, A35; ::_thesis: verum end; then reconsider b = the multF of (product F) || A as BinOp of A by FUNCT_2:def_1, RELSET_1:4; set H = multMagma(# A,b #); multMagma(# A,b #) is Group-like proof reconsider e = g as Element of multMagma(# A,b #) by A3, A5; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# A,b #) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# A,b #) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of multMagma(# A,b #); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st ( h * b1 = e & b1 * h = e ) ) h in the carrier of multMagma(# A,b #) ; then reconsider h1 = h as Element of (product F) by A4; [h,e] in [:A,A:] by ZFMISC_1:87; hence h * e = h1 * (1_ (product F)) by FUNCT_1:49 .= h by GROUP_1:def_4 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st ( h * b1 = e & b1 * h = e ) ) [e,h] in [:A,A:] by ZFMISC_1:87; hence e * h = (1_ (product F)) * h1 by FUNCT_1:49 .= h by GROUP_1:def_4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# A,b #) st ( h * b1 = e & b1 * h = e ) reconsider h2 = h1, hh = h1 " as Element of product (Carrier F) by Def2; A71: S1[h1 " ] proof consider J being finite Subset of I, f being ManySortedSet of J such that A72: h = g +* f and A73: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) by A3; defpred S2[ set , set ] means ex G being Group ex m being Element of G st ( G = F . \$1 & m = f . \$1 & \$2 = m " ); A74: for i being set st i in J holds ex j being set st S2[i,j] proof let i be set ; ::_thesis: ( i in J implies ex j being set st S2[i,j] ) assume A75: i in J ; ::_thesis: ex j being set st S2[i,j] then consider Gg being non empty Group-like multMagma such that A76: Gg = F . i by Def3; ex Ga being non empty associative multMagma st Ga = F . i by A75, Def4; then reconsider G = Gg as Group by A76; ex GG being non empty Group-like multMagma st ( GG = F . i & f . i in the carrier of GG & f . i <> 1_ GG ) by A73, A75; then reconsider m = f . i as Element of G by A76; take m " ; ::_thesis: S2[i,m " ] thus S2[i,m " ] by A76; ::_thesis: verum end; consider f9 being ManySortedSet of J such that A77: for j being set st j in J holds S2[j,f9 . j] from PBOOLE:sch_3(A74); set gf9 = g +* f9; A78: dom f9 = J by PARTFUN1:def_2; A79: dom f = J by PARTFUN1:def_2; A80: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ hh_._i_=_(g_+*_f9)_._i let i be set ; ::_thesis: ( i in I implies hh . b1 = (g +* f9) . b1 ) assume A81: i in I ; ::_thesis: hh . b1 = (g +* f9) . b1 then consider G3 being non empty Group-like multMagma such that A82: G3 = F . i by Def3; ex G4 being non empty associative multMagma st G4 = F . i by A81, Def4; then consider G5 being Group such that A83: G5 = F . i by A82; percases ( i in J or not i in J ) ; supposeA84: i in J ; ::_thesis: hh . b1 = (g +* f9) . b1 then A85: (g +* f9) . i = f9 . i by A78, FUNCT_4:13; A86: ex G being Group ex m being Element of G st ( G = F . i & m = f . i & f9 . i = m " ) by A77, A84; h2 . i = f . i by A72, A79, A84, FUNCT_4:13; hence hh . i = (g +* f9) . i by A81, A86, A85, Th11; ::_thesis: verum end; supposeA87: not i in J ; ::_thesis: hh . b1 = (g +* f9) . b1 then A88: (g +* f9) . i = g . i by A78, FUNCT_4:11 .= 1_ G3 by A81, A82, Th9 ; A89: 1_ G5 = (1_ G5) " by GROUP_1:8; h2 . i = g . i by A72, A79, A87, FUNCT_4:11 .= 1_ G3 by A81, A82, Th9 ; hence hh . i = (g +* f9) . i by A81, A82, A83, A88, A89, Th11; ::_thesis: verum end; end; end; take J ; ::_thesis: ex f being ManySortedSet of J st ( h1 " = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) take f9 ; ::_thesis: ( h1 " = g +* f9 & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) ) ) A90: dom hh = I by A6; dom (g +* f9) = (dom g) \/ (dom f9) by FUNCT_4:def_1 .= I by A2, A1, A78, XBOOLE_1:12 ; hence h1 " = g +* f9 by A90, A80, FUNCT_1:2; ::_thesis: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) ) assume A91: j in J ; ::_thesis: ex G being non empty Group-like multMagma st ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) then consider G being Group, m being Element of G such that A92: G = F . j and A93: m = f . j and A94: f9 . j = m " by A77; take G ; ::_thesis: ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) thus ( G = F . j & f9 . j in the carrier of G ) by A92, A94; ::_thesis: f9 . j <> 1_ G ex G1 being non empty Group-like multMagma st ( G1 = F . j & f . j in the carrier of G1 & f . j <> 1_ G1 ) by A73, A91; hence f9 . j <> 1_ G by A92, A93, A94, GROUP_1:10; ::_thesis: verum end; product (Carrier F) = the carrier of (product F) by Def2; then reconsider h9 = h1 " as Element of multMagma(# A,b #) by A3, A71; take h9 ; ::_thesis: ( h * h9 = e & h9 * h = e ) [h,h9] in [:A,A:] by ZFMISC_1:87; hence h * h9 = h1 * (h1 ") by FUNCT_1:49 .= e by GROUP_1:def_5 ; ::_thesis: h9 * h = e [h9,h] in [:A,A:] by ZFMISC_1:87; hence h9 * h = (h1 ") * h1 by FUNCT_1:49 .= e by GROUP_1:def_5 ; ::_thesis: verum end; then reconsider H = multMagma(# A,b #) as non empty Group-like multMagma ; reconsider H = H as strict Subgroup of product F by A4, GROUP_2:def_5; take H ; ::_thesis: for x being set holds ( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) let x be set ; ::_thesis: ( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) hereby ::_thesis: ( ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) implies x in the carrier of H ) assume x in the carrier of H ; ::_thesis: ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) then S1[x] by A3; hence ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ; ::_thesis: verum end; given g being Element of product (Carrier F), J being finite Subset of I, f being ManySortedSet of J such that A95: g = 1_ (product F) and A96: x = g +* f and A97: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; ::_thesis: x in the carrier of H A98: dom g = I by A6; set gf = g +* f; A99: dom f = J by PARTFUN1:def_2; A100: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (g_+*_f)_._i_in_(Carrier_F)_._i let i be set ; ::_thesis: ( i in I implies (g +* f) . b1 in (Carrier F) . b1 ) assume A101: i in I ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1 then A102: ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; percases ( i in J or not i in J ) ; supposeA103: i in J ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1 then ex G being non empty Group-like multMagma st ( G = F . i & f . i in the carrier of G & f . i <> 1_ G ) by A97; hence (g +* f) . i in (Carrier F) . i by A99, A102, A103, FUNCT_4:13; ::_thesis: verum end; supposeA104: not i in J ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1 consider G being non empty Group-like multMagma such that A105: G = F . i by A101, Def3; (g +* f) . i = g . i by A99, A104, FUNCT_4:11 .= 1_ G by A95, A101, A105, Th9 ; hence (g +* f) . i in (Carrier F) . i by A102, A105; ::_thesis: verum end; end; end; dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1 .= I by A98, A99, XBOOLE_1:12 ; then x in product (Carrier F) by A1, A96, A100, CARD_3:9; hence x in the carrier of H by A3, A95, A96, A97; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of product F st ( for x being set holds ( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being set holds ( x in the carrier of b2 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & \$1 = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ); let A, B be strict Subgroup of product F; ::_thesis: ( ( for x being set holds ( x in the carrier of A iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being set holds ( x in the carrier of B iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) implies A = B ) assume that A106: for x being set holds ( x in the carrier of A iff S1[x] ) and A107: for x being set holds ( x in the carrier of B iff S1[x] ) ; ::_thesis: A = B the carrier of A = the carrier of B from XBOOLE_0:sch_2(A106, A107); hence A = B by GROUP_2:59; ::_thesis: verum end; end; :: deftheorem Def9 defines sum GROUP_7:def_9_:_ for I being set for F being Group-like associative multMagma-Family of I for b3 being strict Subgroup of product F holds ( b3 = sum F iff for x being set holds ( x in the carrier of b3 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ); registration let I be set ; let F be Group-like associative multMagma-Family of I; let f, g be Element of (sum F); cluster the multF of (sum F) . (f,g) -> Relation-like Function-like ; coherence ( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like ) proof A1: the multF of (sum F) . (f,g) in the carrier of (sum F) ; the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def_5; then reconsider h = the multF of (sum F) . (f,g) as Element of product (Carrier F) by A1, Def2; h is Function ; hence ( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like ) ; ::_thesis: verum end; end; theorem :: GROUP_7:9 for I being finite set for F being Group-like associative multMagma-Family of I holds product F = sum F proof let I be finite set ; ::_thesis: for F being Group-like associative multMagma-Family of I holds product F = sum F let F be Group-like associative multMagma-Family of I; ::_thesis: product F = sum F set GP = product F; set S = sum F; A1: the carrier of (sum F) = the carrier of (product F) proof reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2; thus the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def_5; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (product F) c= the carrier of (sum F) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (product F) or x in the carrier of (sum F) ) assume x in the carrier of (product F) ; ::_thesis: x in the carrier of (sum F) then reconsider f = x as Element of product (Carrier F) by Def2; A2: for p being Element of product (Carrier F) holds dom p = I by PARTFUN1:def_2; then A3: dom f = I ; reconsider f = f as ManySortedSet of I ; ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) proof deffunc H1( set ) -> set = f . \$1; defpred S1[ set ] means ex G being non empty Group-like multMagma ex m being Element of G st ( G = F . \$1 & m = f . \$1 & m <> 1_ G ); consider J being set such that A4: for j being set holds ( j in J iff ( j in I & S1[j] ) ) from XBOOLE_0:sch_1(); J c= I proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in J or j in I ) assume j in J ; ::_thesis: j in I hence j in I by A4; ::_thesis: verum end; then reconsider J = J as Subset of I ; consider ff being ManySortedSet of J such that A5: for j being set st j in J holds ff . j = H1(j) from PBOOLE:sch_4(); A6: dom ff = J by PARTFUN1:def_2; A7: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ f_._i_=_(g_+*_ff)_._i let i be set ; ::_thesis: ( i in I implies f . b1 = (g +* ff) . b1 ) assume A8: i in I ; ::_thesis: f . b1 = (g +* ff) . b1 percases ( i in J or not i in J ) ; supposeA9: i in J ; ::_thesis: f . b1 = (g +* ff) . b1 hence f . i = ff . i by A5 .= (g +* ff) . i by A6, A9, FUNCT_4:13 ; ::_thesis: verum end; supposeA10: not i in J ; ::_thesis: f . b1 = (g +* ff) . b1 consider G being non empty Group-like multMagma such that A11: G = F . i by A8, Def3; f . i is Element of G by A8, A11, Lm1; hence f . i = 1_ G by A4, A8, A10, A11 .= g . i by A8, A11, Th9 .= (g +* ff) . i by A6, A10, FUNCT_4:11 ; ::_thesis: verum end; end; end; take g ; ::_thesis: ex J being finite Subset of I ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) take J ; ::_thesis: ex f being ManySortedSet of J st ( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) take ff ; ::_thesis: ( g = 1_ (product F) & x = g +* ff & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) ) thus g = 1_ (product F) ; ::_thesis: ( x = g +* ff & ( for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) ) A12: dom g = I by A2; dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def_1 .= I by A6, A12, XBOOLE_1:12 ; hence x = g +* ff by A3, A7, FUNCT_1:2; ::_thesis: for j being set st j in J holds ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) assume A13: j in J ; ::_thesis: ex G being non empty Group-like multMagma st ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) then consider G being non empty Group-like multMagma , m being Element of G such that A14: G = F . j and A15: m = f . j and A16: m <> 1_ G by A4; take G ; ::_thesis: ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ff . j = f . j by A5, A13; hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by A14, A15, A16; ::_thesis: verum end; hence x in the carrier of (sum F) by Def9; ::_thesis: verum end; product F is Subgroup of product F by GROUP_2:54; hence product F = sum F by A1, GROUP_2:59; ::_thesis: verum end; begin theorem Th13: :: GROUP_7:10 for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1} proof let G1 be non empty multMagma ; ::_thesis: <*G1*> is multMagma-Family of {1} dom <*G1*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8; then reconsider A = <*G1*> as ManySortedSet of {1} by PARTFUN1:def_2, RELAT_1:def_18; A is multMagma-yielding proof let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma ) assume y in rng A ; ::_thesis: y is non empty multMagma then consider x being set such that A2: x in dom A and A3: A . x = y by FUNCT_1:def_3; x = 1 by A2, TARSKI:def_1; hence y is non empty multMagma by A3, FINSEQ_1:def_8; ::_thesis: verum end; hence <*G1*> is multMagma-Family of {1} ; ::_thesis: verum end; registration let G1 be non empty multMagma ; cluster<*G1*> -> {1} -defined ; coherence <*G1*> is {1} -defined by Th13; end; registration let G1 be non empty multMagma ; cluster<*G1*> -> total multMagma-yielding ; coherence ( <*G1*> is total & <*G1*> is multMagma-yielding ) by Th13; end; theorem Th14: :: GROUP_7:11 for G1 being non empty Group-like multMagma holds <*G1*> is Group-like multMagma-Family of {1} proof let G1 be non empty Group-like multMagma ; ::_thesis: <*G1*> is Group-like multMagma-Family of {1} reconsider A = <*G1*> as multMagma-Family of {1} ; A is Group-like proof let x be Element of {1}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like x = 1 by TARSKI:def_1; hence A . x is Group-like by FINSEQ_1:def_8; ::_thesis: verum end; hence <*G1*> is Group-like multMagma-Family of {1} ; ::_thesis: verum end; registration let G1 be non empty Group-like multMagma ; cluster<*G1*> -> Group-like ; coherence <*G1*> is Group-like by Th14; end; theorem Th15: :: GROUP_7:12 for G1 being non empty associative multMagma holds <*G1*> is associative multMagma-Family of {1} proof let G1 be non empty associative multMagma ; ::_thesis: <*G1*> is associative multMagma-Family of {1} reconsider A = <*G1*> as multMagma-Family of {1} ; A is associative proof let x be Element of {1}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative x = 1 by TARSKI:def_1; hence A . x is associative by FINSEQ_1:def_8; ::_thesis: verum end; hence <*G1*> is associative multMagma-Family of {1} ; ::_thesis: verum end; registration let G1 be non empty associative multMagma ; cluster<*G1*> -> associative ; coherence <*G1*> is associative by Th15; end; theorem Th16: :: GROUP_7:13 for G1 being non empty commutative multMagma holds <*G1*> is commutative multMagma-Family of {1} proof let G1 be non empty commutative multMagma ; ::_thesis: <*G1*> is commutative multMagma-Family of {1} reconsider A = <*G1*> as multMagma-Family of {1} ; A is commutative proof let x be Element of {1}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative x = 1 by TARSKI:def_1; hence A . x is commutative by FINSEQ_1:def_8; ::_thesis: verum end; hence <*G1*> is commutative multMagma-Family of {1} ; ::_thesis: verum end; registration let G1 be non empty commutative multMagma ; cluster<*G1*> -> commutative ; coherence <*G1*> is commutative by Th16; end; theorem :: GROUP_7:14 for G1 being Group holds <*G1*> is Group-like associative multMagma-Family of {1} ; theorem :: GROUP_7:15 for G1 being commutative Group holds <*G1*> is Group-like associative commutative multMagma-Family of {1} ; registration let G1 be non empty multMagma ; cluster -> FinSequence-like for Element of product (Carrier <*G1*>); coherence for b1 being Element of product (Carrier <*G1*>) holds b1 is FinSequence-like proof let x be Element of product (Carrier <*G1*>); ::_thesis: x is FinSequence-like take 1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 1 thus dom x = dom (Carrier <*G1*>) by CARD_3:9 .= Seg 1 by FINSEQ_1:2, PARTFUN1:def_2 ; ::_thesis: verum end; end; registration let G1 be non empty multMagma ; cluster -> FinSequence-like for Element of the carrier of (product <*G1*>); coherence for b1 being Element of (product <*G1*>) holds b1 is FinSequence-like proof let x be Element of (product <*G1*>); ::_thesis: x is FinSequence-like reconsider y = x as Element of product (Carrier <*G1*>) by Def2; y is FinSequence-like ; hence x is FinSequence-like ; ::_thesis: verum end; end; definition let G1 be non empty multMagma ; let x be Element of G1; :: original: <* redefine func<*x*> -> Element of (product <*G1*>); coherence <*x*> is Element of (product <*G1*>) proof set xy = <*x*>; set G = <*G1*>; A1: dom (Carrier <*G1*>) = {1} by PARTFUN1:def_2; A2: <*G1*> . 1 = G1 by FINSEQ_1:def_8; A3: <*x*> . 1 = x by FINSEQ_1:def_8; A4: for a being set st a in {1} holds <*x*> . a in (Carrier <*G1*>) . a proof let a be set ; ::_thesis: ( a in {1} implies <*x*> . a in (Carrier <*G1*>) . a ) assume A5: a in {1} ; ::_thesis: <*x*> . a in (Carrier <*G1*>) . a then A6: a = 1 by TARSKI:def_1; then ex R being 1-sorted st ( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by A5, PRALG_1:def_13; hence <*x*> . a in (Carrier <*G1*>) . a by A3, A2, A6; ::_thesis: verum end; dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8; then <*x*> in product (Carrier <*G1*>) by A1, A4, CARD_3:9; hence <*x*> is Element of (product <*G1*>) by Def2; ::_thesis: verum end; end; theorem Th19: :: GROUP_7:16 for G1, G2 being non empty multMagma holds <*G1,G2*> is multMagma-Family of {1,2} proof let G1, G2 be non empty multMagma ; ::_thesis: <*G1,G2*> is multMagma-Family of {1,2} dom <*G1,G2*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then reconsider A = <*G1,G2*> as ManySortedSet of {1,2} by PARTFUN1:def_2, RELAT_1:def_18; A is multMagma-yielding proof let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma ) assume y in rng A ; ::_thesis: y is non empty multMagma then consider x being set such that A2: x in dom A and A3: A . x = y by FUNCT_1:def_3; ( x = 1 or x = 2 ) by A2, TARSKI:def_2; hence y is non empty multMagma by A3, FINSEQ_1:44; ::_thesis: verum end; hence <*G1,G2*> is multMagma-Family of {1,2} ; ::_thesis: verum end; registration let G1, G2 be non empty multMagma ; cluster<*G1,G2*> -> {1,2} -defined ; coherence <*G1,G2*> is {1,2} -defined by Th19; end; registration let G1, G2 be non empty multMagma ; cluster<*G1,G2*> -> total multMagma-yielding ; coherence ( <*G1,G2*> is total & <*G1,G2*> is multMagma-yielding ) by Th19; end; theorem Th20: :: GROUP_7:17 for G1, G2 being non empty Group-like multMagma holds <*G1,G2*> is Group-like multMagma-Family of {1,2} proof let G1, G2 be non empty Group-like multMagma ; ::_thesis: <*G1,G2*> is Group-like multMagma-Family of {1,2} reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ; A is Group-like proof let x be Element of {1,2}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like ( x = 1 or x = 2 ) by TARSKI:def_2; hence A . x is Group-like by FINSEQ_1:44; ::_thesis: verum end; hence <*G1,G2*> is Group-like multMagma-Family of {1,2} ; ::_thesis: verum end; registration let G1, G2 be non empty Group-like multMagma ; cluster<*G1,G2*> -> Group-like ; coherence <*G1,G2*> is Group-like by Th20; end; theorem Th21: :: GROUP_7:18 for G1, G2 being non empty associative multMagma holds <*G1,G2*> is associative multMagma-Family of {1,2} proof let G1, G2 be non empty associative multMagma ; ::_thesis: <*G1,G2*> is associative multMagma-Family of {1,2} reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ; A is associative proof let x be Element of {1,2}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative ( x = 1 or x = 2 ) by TARSKI:def_2; hence A . x is associative by FINSEQ_1:44; ::_thesis: verum end; hence <*G1,G2*> is associative multMagma-Family of {1,2} ; ::_thesis: verum end; registration let G1, G2 be non empty associative multMagma ; cluster<*G1,G2*> -> associative ; coherence <*G1,G2*> is associative by Th21; end; theorem Th22: :: GROUP_7:19 for G1, G2 being non empty commutative multMagma holds <*G1,G2*> is commutative multMagma-Family of {1,2} proof let G1, G2 be non empty commutative multMagma ; ::_thesis: <*G1,G2*> is commutative multMagma-Family of {1,2} reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ; A is commutative proof let x be Element of {1,2}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative ( x = 1 or x = 2 ) by TARSKI:def_2; hence A . x is commutative by FINSEQ_1:44; ::_thesis: verum end; hence <*G1,G2*> is commutative multMagma-Family of {1,2} ; ::_thesis: verum end; registration let G1, G2 be non empty commutative multMagma ; cluster<*G1,G2*> -> commutative ; coherence <*G1,G2*> is commutative by Th22; end; theorem :: GROUP_7:20 for G1, G2 being Group holds <*G1,G2*> is Group-like associative multMagma-Family of {1,2} ; theorem :: GROUP_7:21 for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative multMagma-Family of {1,2} ; registration let G1, G2 be non empty multMagma ; cluster -> FinSequence-like for Element of product (Carrier <*G1,G2*>); coherence for b1 being Element of product (Carrier <*G1,G2*>) holds b1 is FinSequence-like proof let x be Element of product (Carrier <*G1,G2*>); ::_thesis: x is FinSequence-like take 2 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 2 thus dom x = dom (Carrier <*G1,G2*>) by CARD_3:9 .= Seg 2 by FINSEQ_1:2, PARTFUN1:def_2 ; ::_thesis: verum end; end; registration let G1, G2 be non empty multMagma ; cluster -> FinSequence-like for Element of the carrier of (product <*G1,G2*>); coherence for b1 being Element of (product <*G1,G2*>) holds b1 is FinSequence-like proof let x be Element of (product <*G1,G2*>); ::_thesis: x is FinSequence-like reconsider y = x as Element of product (Carrier <*G1,G2*>) by Def2; y is FinSequence-like ; hence x is FinSequence-like ; ::_thesis: verum end; end; definition let G1, G2 be non empty multMagma ; let x be Element of G1; let y be Element of G2; :: original: <* redefine func<*x,y*> -> Element of (product <*G1,G2*>); coherence <*x,y*> is Element of (product <*G1,G2*>) proof set xy = <*x,y*>; set G = <*G1,G2*>; A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def_2; A2: <*x,y*> . 2 = y by FINSEQ_1:44; A3: <*G1,G2*> . 2 = G2 by FINSEQ_1:44; A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44; A5: <*x,y*> . 1 = x by FINSEQ_1:44; A6: for a being set st a in {1,2} holds <*x,y*> . a in (Carrier <*G1,G2*>) . a proof let a be set ; ::_thesis: ( a in {1,2} implies <*x,y*> . a in (Carrier <*G1,G2*>) . a ) assume A7: a in {1,2} ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a percases ( a = 1 or a = 2 ) by A7, TARSKI:def_2; supposeA8: a = 1 ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a then ex R being 1-sorted st ( R = <*G1,G2*> . 1 & (Carrier <*G1,G2*>) . 1 = the carrier of R ) by A7, PRALG_1:def_13; hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A5, A4, A8; ::_thesis: verum end; supposeA9: a = 2 ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a then ex R being 1-sorted st ( R = <*G1,G2*> . 2 & (Carrier <*G1,G2*>) . 2 = the carrier of R ) by A7, PRALG_1:def_13; hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A2, A3, A9; ::_thesis: verum end; end; end; dom <*x,y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then <*x,y*> in product (Carrier <*G1,G2*>) by A1, A6, CARD_3:9; hence <*x,y*> is Element of (product <*G1,G2*>) by Def2; ::_thesis: verum end; end; theorem Th25: :: GROUP_7:22 for G1, G2, G3 being non empty multMagma holds <*G1,G2,G3*> is multMagma-Family of {1,2,3} proof let G1, G2, G3 be non empty multMagma ; ::_thesis: <*G1,G2,G3*> is multMagma-Family of {1,2,3} dom <*G1,G2,G3*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1; then reconsider A = <*G1,G2,G3*> as ManySortedSet of {1,2,3} by PARTFUN1:def_2, RELAT_1:def_18; A is multMagma-yielding proof let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma ) assume y in rng A ; ::_thesis: y is non empty multMagma then consider x being set such that A2: x in dom A and A3: A . x = y by FUNCT_1:def_3; ( x = 1 or x = 2 or x = 3 ) by A2, ENUMSET1:def_1; hence y is non empty multMagma by A3, FINSEQ_1:45; ::_thesis: verum end; hence <*G1,G2,G3*> is multMagma-Family of {1,2,3} ; ::_thesis: verum end; registration let G1, G2, G3 be non empty multMagma ; cluster<*G1,G2,G3*> -> {1,2,3} -defined ; coherence <*G1,G2,G3*> is {1,2,3} -defined by Th25; end; registration let G1, G2, G3 be non empty multMagma ; cluster<*G1,G2,G3*> -> total multMagma-yielding ; coherence ( <*G1,G2,G3*> is total & <*G1,G2,G3*> is multMagma-yielding ) by Th25; end; theorem Th26: :: GROUP_7:23 for G1, G2, G3 being non empty Group-like multMagma holds <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3} proof let G1, G2, G3 be non empty Group-like multMagma ; ::_thesis: <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3} reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ; A is Group-like proof let x be Element of {1,2,3}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1; hence A . x is Group-like by FINSEQ_1:45; ::_thesis: verum end; hence <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3} ; ::_thesis: verum end; registration let G1, G2, G3 be non empty Group-like multMagma ; cluster<*G1,G2,G3*> -> Group-like ; coherence <*G1,G2,G3*> is Group-like by Th26; end; theorem Th27: :: GROUP_7:24 for G1, G2, G3 being non empty associative multMagma holds <*G1,G2,G3*> is associative multMagma-Family of {1,2,3} proof let G1, G2, G3 be non empty associative multMagma ; ::_thesis: <*G1,G2,G3*> is associative multMagma-Family of {1,2,3} reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ; A is associative proof let x be Element of {1,2,3}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1; hence A . x is associative by FINSEQ_1:45; ::_thesis: verum end; hence <*G1,G2,G3*> is associative multMagma-Family of {1,2,3} ; ::_thesis: verum end; registration let G1, G2, G3 be non empty associative multMagma ; cluster<*G1,G2,G3*> -> associative ; coherence <*G1,G2,G3*> is associative by Th27; end; theorem Th28: :: GROUP_7:25 for G1, G2, G3 being non empty commutative multMagma holds <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3} proof let G1, G2, G3 be non empty commutative multMagma ; ::_thesis: <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3} reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ; A is commutative proof let x be Element of {1,2,3}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1; hence A . x is commutative by FINSEQ_1:45; ::_thesis: verum end; hence <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3} ; ::_thesis: verum end; registration let G1, G2, G3 be non empty commutative multMagma ; cluster<*G1,G2,G3*> -> commutative ; coherence <*G1,G2,G3*> is commutative by Th28; end; theorem :: GROUP_7:26 for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3} ; theorem :: GROUP_7:27 for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is Group-like associative commutative multMagma-Family of {1,2,3} ; registration let G1, G2, G3 be non empty multMagma ; cluster -> FinSequence-like for Element of product (Carrier <*G1,G2,G3*>); coherence for b1 being Element of product (Carrier <*G1,G2,G3*>) holds b1 is FinSequence-like proof let x be Element of product (Carrier <*G1,G2,G3*>); ::_thesis: x is FinSequence-like take 3 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 3 thus dom x = dom (Carrier <*G1,G2,G3*>) by CARD_3:9 .= Seg 3 by FINSEQ_3:1, PARTFUN1:def_2 ; ::_thesis: verum end; end; registration let G1, G2, G3 be non empty multMagma ; cluster -> FinSequence-like for Element of the carrier of (product <*G1,G2,G3*>); coherence for b1 being Element of (product <*G1,G2,G3*>) holds b1 is FinSequence-like proof let x be Element of (product <*G1,G2,G3*>); ::_thesis: x is FinSequence-like reconsider y = x as Element of product (Carrier <*G1,G2,G3*>) by Def2; y is FinSequence-like ; hence x is FinSequence-like ; ::_thesis: verum end; end; definition let G1, G2, G3 be non empty multMagma ; let x be Element of G1; let y be Element of G2; let z be Element of G3; :: original: <* redefine func<*x,y,z*> -> Element of (product <*G1,G2,G3*>); coherence <*x,y,z*> is Element of (product <*G1,G2,G3*>) proof set xy = <*x,y,z*>; set G = <*G1,G2,G3*>; A1: dom (Carrier <*G1,G2,G3*>) = {1,2,3} by PARTFUN1:def_2; A2: <*x,y,z*> . 2 = y by FINSEQ_1:45; A3: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45; A4: <*x,y,z*> . 3 = z by FINSEQ_1:45; A5: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45; A6: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45; A7: <*x,y,z*> . 1 = x by FINSEQ_1:45; A8: for a being set st a in {1,2,3} holds <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a proof let a be set ; ::_thesis: ( a in {1,2,3} implies <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a ) assume A9: a in {1,2,3} ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a percases ( a = 1 or a = 2 or a = 3 ) by A9, ENUMSET1:def_1; supposeA10: a = 1 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a then ex R being 1-sorted st ( R = <*G1,G2,G3*> . 1 & (Carrier <*G1,G2,G3*>) . 1 = the carrier of R ) by A9, PRALG_1:def_13; hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A7, A3, A10; ::_thesis: verum end; supposeA11: a = 2 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a then ex R being 1-sorted st ( R = <*G1,G2,G3*> . 2 & (Carrier <*G1,G2,G3*>) . 2 = the carrier of R ) by A9, PRALG_1:def_13; hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A2, A6, A11; ::_thesis: verum end; supposeA12: a = 3 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a then ex R being 1-sorted st ( R = <*G1,G2,G3*> . 3 & (Carrier <*G1,G2,G3*>) . 3 = the carrier of R ) by A9, PRALG_1:def_13; hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A4, A5, A12; ::_thesis: verum end; end; end; dom <*x,y,z*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1; then <*x,y,z*> in product (Carrier <*G1,G2,G3*>) by A1, A8, CARD_3:9; hence <*x,y,z*> is Element of (product <*G1,G2,G3*>) by Def2; ::_thesis: verum end; end; theorem Th31: :: GROUP_7:28 for G1 being non empty multMagma for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*> proof let G1 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*> let x1, x2 be Element of G1; ::_thesis: <*x1*> * <*x2*> = <*(x1 * x2)*> set G = <*G1*>; A1: <*G1*> . 1 = G1 by FINSEQ_1:def_8; reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2; A2: l . 1 = x1 by FINSEQ_1:def_8; A3: p . 1 = x2 by FINSEQ_1:def_8; A4: lpp . 1 = x1 * x2 by FINSEQ_1:def_8; A5: 1 in {1} by TARSKI:def_1; A6: for k being Nat st 1 <= k & k <= 1 holds lpl . k = lpp . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= 1 implies lpl . k = lpp . k ) assume that A7: 1 <= k and A8: k <= 1 ; ::_thesis: lpl . k = lpp . k k in NAT by ORDINAL1:def_12; then k in Seg 1 by A7, A8; then k = 1 by FINSEQ_1:2, TARSKI:def_1; hence lpl . k = lpp . k by A5, A2, A3, A1, A4, Th4; ::_thesis: verum end; dom lpl = dom (Carrier <*G1*>) by CARD_3:9 .= Seg 1 by FINSEQ_1:2, PARTFUN1:def_2 ; then A9: len lpl = 1 by FINSEQ_1:def_3; len lpp = 1 by FINSEQ_1:39; hence <*x1*> * <*x2*> = <*(x1 * x2)*> by A9, A6, FINSEQ_1:14; ::_thesis: verum end; theorem :: GROUP_7:29 for G1, G2 being non empty multMagma for x1, x2 being Element of G1 for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> proof let G1, G2 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1 for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> let x1, x2 be Element of G1; ::_thesis: for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> let y1, y2 be Element of G2; ::_thesis: <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> set G = <*G1,G2*>; A1: <*G1,G2*> . 1 = G1 by FINSEQ_1:44; A2: <*G1,G2*> . 2 = G2 by FINSEQ_1:44; reconsider l = <*x1,y1*>, p = <*x2,y2*>, lpl = <*x1,y1*> * <*x2,y2*>, lpp = <*(x1 * x2),(y1 * y2)*> as Element of product (Carrier <*G1,G2*>) by Def2; A3: 2 in {1,2} by TARSKI:def_2; A4: l . 1 = x1 by FINSEQ_1:44; A5: lpp . 1 = x1 * x2 by FINSEQ_1:44; A6: p . 2 = y2 by FINSEQ_1:44; A7: lpp . 2 = y1 * y2 by FINSEQ_1:44; A8: p . 1 = x2 by FINSEQ_1:44; A9: l . 2 = y1 by FINSEQ_1:44; A10: 1 in {1,2} by TARSKI:def_2; A11: for k being Nat st 1 <= k & k <= 2 holds lpl . k = lpp . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= 2 implies lpl . k = lpp . k ) assume that A12: 1 <= k and A13: k <= 2 ; ::_thesis: lpl . k = lpp . k k in NAT by ORDINAL1:def_12; then A14: k in Seg 2 by A12, A13; percases ( k = 1 or k = 2 ) by A14, FINSEQ_1:2, TARSKI:def_2; suppose k = 1 ; ::_thesis: lpl . k = lpp . k hence lpl . k = lpp . k by A10, A4, A8, A1, A5, Th4; ::_thesis: verum end; suppose k = 2 ; ::_thesis: lpl . k = lpp . k hence lpl . k = lpp . k by A3, A9, A6, A2, A7, Th4; ::_thesis: verum end; end; end; dom lpl = dom (Carrier <*G1,G2*>) by CARD_3:9 .= Seg 2 by FINSEQ_1:2, PARTFUN1:def_2 ; then A15: len lpl = 2 by FINSEQ_1:def_3; len lpp = 2 by FINSEQ_1:44; hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A15, A11, FINSEQ_1:14; ::_thesis: verum end; theorem :: GROUP_7:30 for G1, G2, G3 being non empty multMagma for x1, x2 being Element of G1 for y1, y2 being Element of G2 for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> proof let G1, G2, G3 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1 for y1, y2 being Element of G2 for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> let x1, x2 be Element of G1; ::_thesis: for y1, y2 being Element of G2 for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> let y1, y2 be Element of G2; ::_thesis: for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> let z1, z2 be Element of G3; ::_thesis: <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> set G = <*G1,G2,G3*>; A1: 3 in {1,2,3} by ENUMSET1:def_1; A2: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45; A3: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45; A4: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45; reconsider l = <*x1,y1,z1*>, p = <*x2,y2,z2*>, lpl = <*x1,y1,z1*> * <*x2,y2,z2*>, lpp = <*(x1 * x2),(y1 * y2),(z1 * z2)*> as Element of product (Carrier <*G1,G2,G3*>) by Def2; A5: 2 in {1,2,3} by ENUMSET1:def_1; A6: l . 1 = x1 by FINSEQ_1:45; A7: l . 3 = z1 by FINSEQ_1:45; A8: l . 2 = y1 by FINSEQ_1:45; A9: lpp . 3 = z1 * z2 by FINSEQ_1:45; A10: lpp . 2 = y1 * y2 by FINSEQ_1:45; A11: lpp . 1 = x1 * x2 by FINSEQ_1:45; A12: p . 3 = z2 by FINSEQ_1:45; A13: p . 2 = y2 by FINSEQ_1:45; A14: p . 1 = x2 by FINSEQ_1:45; A15: 1 in {1,2,3} by ENUMSET1:def_1; A16: for k being Nat st 1 <= k & k <= 3 holds lpl . k = lpp . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= 3 implies lpl . k = lpp . k ) assume that A17: 1 <= k and A18: k <= 3 ; ::_thesis: lpl . k = lpp . k k in NAT by ORDINAL1:def_12; then A19: k in Seg 3 by A17, A18; percases ( k = 1 or k = 2 or k = 3 ) by A19, ENUMSET1:def_1, FINSEQ_3:1; suppose k = 1 ; ::_thesis: lpl . k = lpp . k hence lpl . k = lpp . k by A15, A6, A14, A2, A11, Th4; ::_thesis: verum end; suppose k = 2 ; ::_thesis: lpl . k = lpp . k hence lpl . k = lpp . k by A5, A8, A13, A4, A10, Th4; ::_thesis: verum end; suppose k = 3 ; ::_thesis: lpl . k = lpp . k hence lpl . k = lpp . k by A1, A7, A12, A3, A9, Th4; ::_thesis: verum end; end; end; dom lpl = dom (Carrier <*G1,G2,G3*>) by CARD_3:9 .= Seg 3 by FINSEQ_3:1, PARTFUN1:def_2 ; then A20: len lpl = 3 by FINSEQ_1:def_3; len lpp = 3 by FINSEQ_1:45; hence <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> by A20, A16, FINSEQ_1:14; ::_thesis: verum end; theorem :: GROUP_7:31 for G1 being non empty Group-like multMagma holds 1_ (product <*G1*>) = <*(1_ G1)*> proof let G1 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1*>) = <*(1_ G1)*> set s = <*(1_ G1)*>; set f = <*G1*>; dom <*(1_ G1)*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8; then reconsider s = <*(1_ G1)*> as ManySortedSet of {1} by PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in {1} holds ex G being non empty Group-like multMagma st ( G = <*G1*> . i & s . i = 1_ G ) proof let i be set ; ::_thesis: ( i in {1} implies ex G being non empty Group-like multMagma st ( G = <*G1*> . i & s . i = 1_ G ) ) assume i in {1} ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1*> . i & s . i = 1_ G ) then A1: i = 1 by TARSKI:def_1; then reconsider G = <*G1*> . i as non empty Group-like multMagma by FINSEQ_1:def_8; take G ; ::_thesis: ( G = <*G1*> . i & s . i = 1_ G ) <*G1*> . i = G1 by A1, FINSEQ_1:def_8; hence ( G = <*G1*> . i & s . i = 1_ G ) by A1, FINSEQ_1:def_8; ::_thesis: verum end; hence 1_ (product <*G1*>) = <*(1_ G1)*> by Th8; ::_thesis: verum end; theorem :: GROUP_7:32 for G1, G2 being non empty Group-like multMagma holds 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*> proof let G1, G2 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*> set s = <*(1_ G1),(1_ G2)*>; set f = <*G1,G2*>; dom <*(1_ G1),(1_ G2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then reconsider s = <*(1_ G1),(1_ G2)*> as ManySortedSet of {1,2} by PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in {1,2} holds ex G being non empty Group-like multMagma st ( G = <*G1,G2*> . i & s . i = 1_ G ) proof let i be set ; ::_thesis: ( i in {1,2} implies ex G being non empty Group-like multMagma st ( G = <*G1,G2*> . i & s . i = 1_ G ) ) assume A1: i in {1,2} ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2*> . i & s . i = 1_ G ) percases ( i = 1 or i = 2 ) by A1, TARSKI:def_2; supposeA2: i = 1 ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2*> . i & s . i = 1_ G ) then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:44; take G ; ::_thesis: ( G = <*G1,G2*> . i & s . i = 1_ G ) <*G1,G2*> . i = G1 by A2, FINSEQ_1:44; hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A2, FINSEQ_1:44; ::_thesis: verum end; supposeA3: i = 2 ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2*> . i & s . i = 1_ G ) then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:44; take G ; ::_thesis: ( G = <*G1,G2*> . i & s . i = 1_ G ) <*G1,G2*> . i = G2 by A3, FINSEQ_1:44; hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A3, FINSEQ_1:44; ::_thesis: verum end; end; end; hence 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*> by Th8; ::_thesis: verum end; theorem :: GROUP_7:33 for G1, G2, G3 being non empty Group-like multMagma holds 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*> proof let G1, G2, G3 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*> set s = <*(1_ G1),(1_ G2),(1_ G3)*>; set f = <*G1,G2,G3*>; dom <*(1_ G1),(1_ G2),(1_ G3)*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1; then reconsider s = <*(1_ G1),(1_ G2),(1_ G3)*> as ManySortedSet of {1,2,3} by PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in {1,2,3} holds ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) proof let i be set ; ::_thesis: ( i in {1,2,3} implies ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) ) assume A1: i in {1,2,3} ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) percases ( i = 1 or i = 2 or i = 3 ) by A1, ENUMSET1:def_1; supposeA2: i = 1 ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45; take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) <*G1,G2,G3*> . i = G1 by A2, FINSEQ_1:45; hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A2, FINSEQ_1:45; ::_thesis: verum end; supposeA3: i = 2 ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45; take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) <*G1,G2,G3*> . i = G2 by A3, FINSEQ_1:45; hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A3, FINSEQ_1:45; ::_thesis: verum end; supposeA4: i = 3 ; ::_thesis: ex G being non empty Group-like multMagma st ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45; take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) <*G1,G2,G3*> . i = G3 by A4, FINSEQ_1:45; hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A4, FINSEQ_1:45; ::_thesis: verum end; end; end; hence 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*> by Th8; ::_thesis: verum end; theorem :: GROUP_7:34 for G1 being Group for x being Element of G1 holds <*x*> " = <*(x ")*> proof let G1 be Group; ::_thesis: for x being Element of G1 holds <*x*> " = <*(x ")*> let x be Element of G1; ::_thesis: <*x*> " = <*(x ")*> reconsider G = <*G1*> as Group-like associative multMagma-Family of {1} ; reconsider lF = <*x*>, p = <*(x ")*> as Element of product (Carrier G) by Def2; A1: p . 1 = x " by FINSEQ_1:def_8; A2: G . 1 = G1 by FINSEQ_1:def_8; for i being set st i in {1} holds ex H being Group ex z being Element of H st ( H = G . i & p . i = z " & z = lF . i ) proof reconsider H = G . 1 as Group by FINSEQ_1:def_8; reconsider z = p . 1 as Element of H by A1, FINSEQ_1:def_8; let i be set ; ::_thesis: ( i in {1} implies ex H being Group ex z being Element of H st ( H = G . i & p . i = z " & z = lF . i ) ) assume A3: i in {1} ; ::_thesis: ex H being Group ex z being Element of H st ( H = G . i & p . i = z " & z = lF . i ) take H ; ::_thesis: ex z being Element of H st ( H = G . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = G . i & p . i = (z ") " & z " = lF . i ) thus H = G . i by A3, TARSKI:def_1; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A3, TARSKI:def_1; ::_thesis: z " = lF . i i = 1 by A3, TARSKI:def_1; hence z " = lF . i by A1, A2, FINSEQ_1:def_8; ::_thesis: verum end; hence <*x*> " = <*(x ")*> by Th10; ::_thesis: verum end; theorem :: GROUP_7:35 for G1, G2 being Group for x being Element of G1 for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*> proof let G1, G2 be Group; ::_thesis: for x being Element of G1 for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*> let x be Element of G1; ::_thesis: for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*> let y be Element of G2; ::_thesis: <*x,y*> " = <*(x "),(y ")*> set G = <*G1,G2*>; A1: <*G1,G2*> . 2 = G2 by FINSEQ_1:44; reconsider lF = <*x,y*>, p = <*(x "),(y ")*> as Element of product (Carrier <*G1,G2*>) by Def2; A2: p . 1 = x " by FINSEQ_1:44; A3: p . 2 = y " by FINSEQ_1:44; A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44; for i being set st i in {1,2} holds ex H being Group ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) proof let i be set ; ::_thesis: ( i in {1,2} implies ex H being Group ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) ) assume A5: i in {1,2} ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) percases ( i = 1 or i = 2 ) by A5, TARSKI:def_2; supposeA6: i = 1 ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) reconsider H = <*G1,G2*> . 1 as Group by FINSEQ_1:44; reconsider z = p . 1 as Element of H by A2, FINSEQ_1:44; take H ; ::_thesis: ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = <*G1,G2*> . i & p . i = (z ") " & z " = lF . i ) thus H = <*G1,G2*> . i by A6; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A6; ::_thesis: z " = lF . i thus z " = lF . i by A2, A4, A6, FINSEQ_1:44; ::_thesis: verum end; supposeA7: i = 2 ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) reconsider H = <*G1,G2*> . 2 as Group by FINSEQ_1:44; reconsider z = p . 2 as Element of H by A3, FINSEQ_1:44; take H ; ::_thesis: ex z being Element of H st ( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = <*G1,G2*> . i & p . i = (z ") " & z " = lF . i ) thus H = <*G1,G2*> . i by A7; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A7; ::_thesis: z " = lF . i thus z " = lF . i by A3, A1, A7, FINSEQ_1:44; ::_thesis: verum end; end; end; hence <*x,y*> " = <*(x "),(y ")*> by Th10; ::_thesis: verum end; theorem :: GROUP_7:36 for G1, G2, G3 being Group for x being Element of G1 for y being Element of G2 for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*> proof let G1, G2, G3 be Group; ::_thesis: for x being Element of G1 for y being Element of G2 for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*> let x be Element of G1; ::_thesis: for y being Element of G2 for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*> let y be Element of G2; ::_thesis: for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*> let z be Element of G3; ::_thesis: <*x,y,z*> " = <*(x "),(y "),(z ")*> set G = <*G1,G2,G3*>; A1: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45; A2: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45; reconsider lF = <*x,y,z*>, p = <*(x "),(y "),(z ")*> as Element of product (Carrier <*G1,G2,G3*>) by Def2; A3: p . 1 = x " by FINSEQ_1:45; A4: p . 3 = z " by FINSEQ_1:45; A5: p . 2 = y " by FINSEQ_1:45; A6: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45; for i being set st i in {1,2,3} holds ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) proof let i be set ; ::_thesis: ( i in {1,2,3} implies ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) ) assume A7: i in {1,2,3} ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) percases ( i = 1 or i = 2 or i = 3 ) by A7, ENUMSET1:def_1; supposeA8: i = 1 ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) reconsider H = <*G1,G2,G3*> . 1 as Group by FINSEQ_1:45; reconsider z = p . 1 as Element of H by A3, FINSEQ_1:45; take H ; ::_thesis: ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i ) thus H = <*G1,G2,G3*> . i by A8; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A8; ::_thesis: z " = lF . i thus z " = lF . i by A3, A6, A8, FINSEQ_1:45; ::_thesis: verum end; supposeA9: i = 2 ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) reconsider H = <*G1,G2,G3*> . 2 as Group by FINSEQ_1:45; reconsider z = p . 2 as Element of H by A5, FINSEQ_1:45; take H ; ::_thesis: ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i ) thus H = <*G1,G2,G3*> . i by A9; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A9; ::_thesis: z " = lF . i thus z " = lF . i by A5, A1, A9, FINSEQ_1:45; ::_thesis: verum end; supposeA10: i = 3 ; ::_thesis: ex H being Group ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) reconsider H = <*G1,G2,G3*> . 3 as Group by FINSEQ_1:45; reconsider z = p . 3 as Element of H by A4, FINSEQ_1:45; take H ; ::_thesis: ex z being Element of H st ( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i ) thus H = <*G1,G2,G3*> . i by A10; ::_thesis: ( p . i = (z ") " & z " = lF . i ) thus p . i = (z ") " by A10; ::_thesis: z " = lF . i thus z " = lF . i by A4, A2, A10, FINSEQ_1:45; ::_thesis: verum end; end; end; hence <*x,y,z*> " = <*(x "),(y "),(z ")*> by Th10; ::_thesis: verum end; theorem Th40: :: GROUP_7:37 for G1 being Group for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds f is Homomorphism of G1,(product <*G1*>) proof let G1 be Group; ::_thesis: for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds f is Homomorphism of G1,(product <*G1*>) let f be Function of the carrier of G1, the carrier of (product <*G1*>); ::_thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is Homomorphism of G1,(product <*G1*>) ) assume A1: for x being Element of G1 holds f . x = <*x*> ; ::_thesis: f is Homomorphism of G1,(product <*G1*>) now__::_thesis:_for_a,_b_being_Element_of_G1_holds_f_._(a_*_b)_=_(f_._a)_*_(f_._b) let a, b be Element of G1; ::_thesis: f . (a * b) = (f . a) * (f . b) thus f . (a * b) = <*(a * b)*> by A1 .= <*a*> * <*b*> by Th31 .= <*a*> * (f . b) by A1 .= (f . a) * (f . b) by A1 ; ::_thesis: verum end; hence f is Homomorphism of G1,(product <*G1*>) by GROUP_6:def_6; ::_thesis: verum end; theorem Th41: :: GROUP_7:38 for G1 being Group for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds f is bijective proof let G1 be Group; ::_thesis: for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds f is bijective let f be Homomorphism of G1,(product <*G1*>); ::_thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is bijective ) assume A1: for x being Element of G1 holds f . x = <*x*> ; ::_thesis: f is bijective A2: dom f = the carrier of G1 by FUNCT_2:def_1; A3: rng f = the carrier of (product <*G1*>) proof thus rng f c= the carrier of (product <*G1*>) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (product <*G1*>) c= rng f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (product <*G1*>) or x in rng f ) assume x in the carrier of (product <*G1*>) ; ::_thesis: x in rng f then reconsider a = x as Element of (product <*G1*>) ; A4: 1 in {1} by TARSKI:def_1; then A5: ex R being 1-sorted st ( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by PRALG_1:def_13; a in the carrier of (product <*G1*>) ; then A6: a in product (Carrier <*G1*>) by Def2; then A7: dom a = dom (Carrier <*G1*>) by CARD_3:9; then A8: dom a = {1} by PARTFUN1:def_2; then a . 1 in (Carrier <*G1*>) . 1 by A6, A7, A4, CARD_3:9; then reconsider b = a . 1 as Element of G1 by A5, FINSEQ_1:def_8; f . b = <*b*> by A1 .= x by A8, FINSEQ_1:2, FINSEQ_1:def_8 ; hence x in rng f by A2, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let m, n be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not m in dom f or not n in dom f or not f . m = f . n or m = n ) assume that A9: m in dom f and A10: n in dom f and A11: f . m = f . n ; ::_thesis: m = n reconsider m1 = m, n1 = n as Element of G1 by A9, A10; <*m1*> = f . m1 by A1 .= <*n1*> by A1, A11 ; hence m = n by FINSEQ_1:76; ::_thesis: verum end; hence f is bijective by A3, GROUP_6:60; ::_thesis: verum end; theorem :: GROUP_7:39 for G1 being Group holds G1, product <*G1*> are_isomorphic proof let G1 be Group; ::_thesis: G1, product <*G1*> are_isomorphic deffunc H1( Element of G1) -> Element of (product <*G1*>) = <*\$1*>; consider f being Function of the carrier of G1, the carrier of (product <*G1*>) such that A1: for x being Element of G1 holds f . x = H1(x) from FUNCT_2:sch_4(); reconsider f = f as Homomorphism of G1,(product <*G1*>) by A1, Th40; take f ; :: according to GROUP_6:def_11 ::_thesis: f is bijective thus f is bijective by A1, Th41; ::_thesis: verum end;