:: GROUP_12 semantic presentation begin registration let I be non empty set ; let F be Group-like multMagma-Family of I; let i be Element of I; clusterF . i -> Group-like for multMagma ; coherence for b1 being multMagma st b1 = F . i holds b1 is Group-like by GROUP_7:def_6; end; registration let I be non empty set ; let F be associative multMagma-Family of I; let i be Element of I; clusterF . i -> associative for multMagma ; coherence for b1 being multMagma st b1 = F . i holds b1 is associative by GROUP_7:def_7; end; registration let I be non empty set ; let F be commutative multMagma-Family of I; let i be Element of I; clusterF . i -> commutative for multMagma ; coherence for b1 being multMagma st b1 = F . i holds b1 is commutative by GROUP_7:def_8; end; theorem Th1: :: GROUP_12:1 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for x being Function for g being Element of (F . i) holds ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for x being Function for g being Element of (F . i) holds ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for x being Function for g being Element of (F . i) holds ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) let i be Element of I; ::_thesis: for x being Function for g being Element of (F . i) holds ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) let x be Function; ::_thesis: for g being Element of (F . i) holds ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) let g be Element of (F . i); ::_thesis: ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) A1: now__::_thesis:_(_x_=_(1__(product_F))_+*_(i,g)_implies_(_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_ x_._j_=_1__(F_._j)_)_)_) assume A2: x = (1_ (product F)) +* (i,g) ; ::_thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; thus A4: dom x = dom (1_ (product F)) by A2, FUNCT_7:30 .= I by A3, PARTFUN1:def_2 ; ::_thesis: ( x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) dom x = dom (1_ (product F)) by A2, FUNCT_7:30; hence x . i = g by A2, A4, FUNCT_7:31; ::_thesis: for j being Element of I st j <> i holds x . j = 1_ (F . j) thus for j being Element of I st j <> i holds x . j = 1_ (F . j) ::_thesis: verum proof let j be Element of I; ::_thesis: ( j <> i implies x . j = 1_ (F . j) ) assume j <> i ; ::_thesis: x . j = 1_ (F . j) then x . j = (1_ (product F)) . j by A2, FUNCT_7:32; hence x . j = 1_ (F . j) by GROUP_7:6; ::_thesis: verum end; end; now__::_thesis:_(_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_ x_._j_=_1__(F_._j)_)_implies_x_=_(1__(product_F))_+*_(i,g)_) assume A5: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ; ::_thesis: x = (1_ (product F)) +* (i,g) the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; then A6: dom (1_ (product F)) = I by PARTFUN1:def_2; A7: dom ((1_ (product F)) +* (i,g)) = dom x by A5, A6, FUNCT_7:30; set FG = (1_ (product F)) +* (i,g); now__::_thesis:_for_j0_being_set_st_j0_in_dom_x_holds_ x_._j0_=_((1__(product_F))_+*_(i,g))_._j0 let j0 be set ; ::_thesis: ( j0 in dom x implies x . b1 = ((1_ (product F)) +* (i,g)) . b1 ) assume j0 in dom x ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1 then reconsider j = j0 as Element of I by A5; percases ( j <> i or j = i ) ; supposeA8: j <> i ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1 then x . j = 1_ (F . j) by A5; hence x . j0 = (1_ (product F)) . j by GROUP_7:6 .= ((1_ (product F)) +* (i,g)) . j0 by A8, FUNCT_7:32 ; ::_thesis: verum end; suppose j = i ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1 hence x . j0 = ((1_ (product F)) +* (i,g)) . j0 by A6, A5, FUNCT_7:31; ::_thesis: verum end; end; end; hence x = (1_ (product F)) +* (i,g) by A7, FUNCT_1:2; ::_thesis: verum end; hence ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) by A1; ::_thesis: verum end; definition let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; func ProjSet (F,i) -> Subset of (product F) means :Def1: :: GROUP_12:def 1 for x being set holds ( x in it iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ); existence ex b1 being Subset of (product F) st for x being set holds ( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) proof set CF = the carrier of (product F); defpred S1[ set ] means ex g being Element of (F . i) st \$1 = (1_ (product F)) +* (i,g); consider H being Subset of the carrier of (product F) such that A1: for x being set holds ( x in H iff ( x in the carrier of (product F) & S1[x] ) ) from SUBSET_1:sch_1(); take H ; ::_thesis: for x being set holds ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) set Gi = F . i; A2: now__::_thesis:_for_x_being_set_st_S1[x]_holds_ x_in_the_carrier_of_(product_F) let x be set ; ::_thesis: ( S1[x] implies x in the carrier of (product F) ) assume A3: S1[x] ; ::_thesis: x in the carrier of (product F) A4: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; ex Ri being 1-sorted st ( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def_13; hence x in the carrier of (product F) by A3, A4, YELLOW17:2; ::_thesis: verum end; let x be set ; ::_thesis: ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ( x in H iff ( x in the carrier of (product F) & S1[x] ) ) by A1; hence ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (product F) st ( for x being set holds ( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds ( x in b2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) holds b1 = b2 proof let F1, F2 be Subset of (product F); ::_thesis: ( ( for x being set holds ( x in F1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds ( x in F2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) implies F1 = F2 ) defpred S1[ set ] means ex g being Element of (F . i) st \$1 = (1_ (product F)) +* (i,g); assume A5: for x being set holds ( x in F1 iff S1[x] ) ; ::_thesis: ( ex x being set st ( ( x in F2 implies ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) implies ( ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & not x in F2 ) ) or F1 = F2 ) assume A6: for x being set holds ( x in F2 iff S1[x] ) ; ::_thesis: F1 = F2 thus F1 = F2 from XBOOLE_0:sch_2(A5, A6); ::_thesis: verum end; end; :: deftheorem Def1 defines ProjSet GROUP_12:def_1_:_ for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for b4 being Subset of (product F) holds ( b4 = ProjSet (F,i) iff for x being set holds ( x in b4 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ); registration let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; cluster ProjSet (F,i) -> non empty ; coherence not ProjSet (F,i) is empty proof set Gi = F . i; the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; then A1: dom (1_ (product F)) = I by PARTFUN1:def_2; A2: dom ((1_ (product F)) +* (i,(1_ (F . i)))) = dom (1_ (product F)) by FUNCT_7:30; set FG = (1_ (product F)) +* (i,(1_ (F . i))); reconsider FG = (1_ (product F)) +* (i,(1_ (F . i))) as I -defined Function by A2, A1, RELAT_1:def_18; now__::_thesis:_for_j_being_Element_of_I_holds_FG_._j_=_1__(F_._j) let j be Element of I; ::_thesis: FG . b1 = 1_ (F . b1) percases ( j <> i or j = i ) ; supposeA3: j <> i ; ::_thesis: FG . b1 = 1_ (F . b1) thus FG . j = (1_ (product F)) . j by A3, FUNCT_7:32 .= 1_ (F . j) by GROUP_7:6 ; ::_thesis: verum end; suppose j = i ; ::_thesis: FG . b1 = 1_ (F . b1) hence FG . j = 1_ (F . j) by A1, FUNCT_7:31; ::_thesis: verum end; end; end; hence not ProjSet (F,i) is empty by Def1; ::_thesis: verum end; end; theorem Th2: :: GROUP_12:2 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for x0 being set holds ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for x0 being set holds ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for x0 being set holds ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) let i be Element of I; ::_thesis: for x0 being set holds ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) let x0 be set ; ::_thesis: ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) defpred S1[ set ] means ex g being Element of (F . i) st \$1 = (1_ (product F)) +* (i,g); A1: now__::_thesis:_(_x0_in_ProjSet_(F,i)_implies_ex_x_being_Function_ex_g_being_Element_of_(F_._i)_st_ (_x_=_x0_&_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_ x_._j_=_1__(F_._j)_)_)_) assume x0 in ProjSet (F,i) ; ::_thesis: ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) then consider g being Element of (F . i) such that A2: x0 = (1_ (product F)) +* (i,g) by Def1; reconsider x = x0 as Function by A2; take x = x; ::_thesis: ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) take g = g; ::_thesis: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) thus x = x0 ; ::_thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) thus ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) by A2, Th1; ::_thesis: verum end; now__::_thesis:_(_ex_x_being_Function_ex_g_being_Element_of_(F_._i)_st_ (_x_=_x0_&_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_ x_._j_=_1__(F_._j)_)_)_implies_x0_in_ProjSet_(F,i)_) assume A3: ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ; ::_thesis: x0 in ProjSet (F,i) thus x0 in ProjSet (F,i) ::_thesis: verum proof consider x being Function, g being Element of (F . i) such that A4: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) by A3; x = (1_ (product F)) +* (i,g) by Th1, A4; hence x0 in ProjSet (F,i) by Def1, A4; ::_thesis: verum end; end; hence ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds x . j = 1_ (F . j) ) ) ) by A1; ::_thesis: verum end; theorem Th3: :: GROUP_12:3 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for g1, g2 being Element of (product F) for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for g1, g2 being Element of (product F) for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for g1, g2 being Element of (product F) for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) let i be Element of I; ::_thesis: for g1, g2 being Element of (product F) for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) let g1, g2 be Element of (product F); ::_thesis: for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) let z1, z2 be Element of (F . i); ::_thesis: ( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) implies g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) ) assume A1: ( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) ) ; ::_thesis: g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) set x1 = g1; set x2 = g2; A2: ( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds g1 . j = 1_ (F . j) ) ) by Th1, A1; A3: ( g2 = g2 & dom g2 = I & g2 . i = z2 & ( for j being Element of I st j <> i holds g2 . j = 1_ (F . j) ) ) by Th1, A1; set x12 = g1 * g2; the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; then A4: dom (g1 * g2) = I by PARTFUN1:def_2; A5: (g1 * g2) . i = z1 * z2 by A2, A3, GROUP_7:1; for j being Element of I st i <> j holds (g1 * g2) . j = 1_ (F . j) proof let j be Element of I; ::_thesis: ( i <> j implies (g1 * g2) . j = 1_ (F . j) ) assume A6: i <> j ; ::_thesis: (g1 * g2) . j = 1_ (F . j) then A7: g1 . j = 1_ (F . j) by Th1, A1; g2 . j = 1_ (F . j) by A6, Th1, A1; hence (g1 * g2) . j = (1_ (F . j)) * (1_ (F . j)) by A7, GROUP_7:1 .= 1_ (F . j) by GROUP_1:def_4 ; ::_thesis: verum end; hence g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by A4, A5, Th1; ::_thesis: verum end; theorem Th4: :: GROUP_12:4 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for g1 being Element of (product F) for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds g1 " = (1_ (product F)) +* (i,(z1 ")) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for g1 being Element of (product F) for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds g1 " = (1_ (product F)) +* (i,(z1 ")) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for g1 being Element of (product F) for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds g1 " = (1_ (product F)) +* (i,(z1 ")) let i be Element of I; ::_thesis: for g1 being Element of (product F) for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds g1 " = (1_ (product F)) +* (i,(z1 ")) let g1 be Element of (product F); ::_thesis: for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds g1 " = (1_ (product F)) +* (i,(z1 ")) let z1 be Element of (F . i); ::_thesis: ( g1 = (1_ (product F)) +* (i,z1) implies g1 " = (1_ (product F)) +* (i,(z1 ")) ) assume A1: g1 = (1_ (product F)) +* (i,z1) ; ::_thesis: g1 " = (1_ (product F)) +* (i,(z1 ")) set x1 = g1; A2: ( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds g1 . j = 1_ (F . j) ) ) by Th1, A1; set x12 = g1 " ; the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; then A3: dom (g1 ") = I by PARTFUN1:def_2; A4: (g1 ") . i = z1 " by A2, GROUP_7:8; A5: for j being Element of I st i <> j holds (g1 ") . j = 1_ (F . j) proof let j be Element of I; ::_thesis: ( i <> j implies (g1 ") . j = 1_ (F . j) ) assume i <> j ; ::_thesis: (g1 ") . j = 1_ (F . j) then g1 . j = 1_ (F . j) by Th1, A1; hence (g1 ") . j = (1_ (F . j)) " by GROUP_7:8 .= 1_ (F . j) by GROUP_1:8 ; ::_thesis: verum end; thus g1 " = (1_ (product F)) +* (i,(z1 ")) by A3, A4, A5, Th1; ::_thesis: verum end; theorem Th5: :: GROUP_12:5 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds g1 * g2 in ProjSet (F,i) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds g1 * g2 in ProjSet (F,i) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds g1 * g2 in ProjSet (F,i) let i be Element of I; ::_thesis: for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds g1 * g2 in ProjSet (F,i) let g1, g2 be Element of (product F); ::_thesis: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) implies g1 * g2 in ProjSet (F,i) ) assume A1: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) ) ; ::_thesis: g1 * g2 in ProjSet (F,i) consider z1 being Element of (F . i) such that A2: g1 = (1_ (product F)) +* (i,z1) by Def1, A1; consider z2 being Element of (F . i) such that A3: g2 = (1_ (product F)) +* (i,z2) by Def1, A1; g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by Th3, A2, A3; hence g1 * g2 in ProjSet (F,i) by Def1; ::_thesis: verum end; theorem Th6: :: GROUP_12:6 for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for g being Element of (product F) st g in ProjSet (F,i) holds g " in ProjSet (F,i) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I for g being Element of (product F) st g in ProjSet (F,i) holds g " in ProjSet (F,i) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I for g being Element of (product F) st g in ProjSet (F,i) holds g " in ProjSet (F,i) let i be Element of I; ::_thesis: for g being Element of (product F) st g in ProjSet (F,i) holds g " in ProjSet (F,i) let g be Element of (product F); ::_thesis: ( g in ProjSet (F,i) implies g " in ProjSet (F,i) ) assume A1: g in ProjSet (F,i) ; ::_thesis: g " in ProjSet (F,i) consider z being Element of (F . i) such that A2: g = (1_ (product F)) +* (i,z) by Def1, A1; g " = (1_ (product F)) +* (i,(z ")) by Th4, A2; hence g " in ProjSet (F,i) by Def1; ::_thesis: verum end; definition let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; func ProjGroup (F,i) -> strict Subgroup of product F means :Def2: :: GROUP_12:def 2 the carrier of it = ProjSet (F,i); existence ex b1 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) proof ( ( for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds g1 * g2 in ProjSet (F,i) ) & ( for g being Element of (product F) st g in ProjSet (F,i) holds g " in ProjSet (F,i) ) ) by Th5, Th6; hence ex b1 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) by GROUP_2:52; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) & the carrier of b2 = ProjSet (F,i) holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def2 defines ProjGroup GROUP_12:def_2_:_ for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for b4 being strict Subgroup of product F holds ( b4 = ProjGroup (F,i) iff the carrier of b4 = ProjSet (F,i) ); Lm1: for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) let i be Element of I; ::_thesis: ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) A1: the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2; defpred S1[ set , set ] means \$2 = (1_ (product F)) +* (i,\$1); A2: for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S1[x,y] proof let x be Element of (F . i); ::_thesis: ex y being Element of (ProjGroup (F,i)) st S1[x,y] (1_ (product F)) +* (i,x) in ProjSet (F,i) by Def1; hence ex y being Element of (ProjGroup (F,i)) st S1[x,y] by A1; ::_thesis: verum end; consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that A3: for x being Element of the carrier of (F . i) holds S1[x,f . x] from FUNCT_2:sch_3(A2); for a, b being Element of (F . i) holds f . (a * b) = (f . a) * (f . b) proof let a, b be Element of (F . i); ::_thesis: f . (a * b) = (f . a) * (f . b) A4: f . a = (1_ (product F)) +* (i,a) by A3; A5: f . b = (1_ (product F)) +* (i,b) by A3; A6: f . (a * b) = (1_ (product F)) +* (i,(a * b)) by A3; the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2; then reconsider ffa = f . a, ffb = f . b as Element of (product F) by TARSKI:def_3; thus (f . a) * (f . b) = ffa * ffb by GROUP_2:43 .= f . (a * b) by A6, A4, A5, Th3 ; ::_thesis: verum end; then reconsider f = f as Homomorphism of (F . i),(ProjGroup (F,i)) by GROUP_6:def_6; take f ; ::_thesis: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(ProjGroup_(F,i))_holds_ x_in_rng_f let x be set ; ::_thesis: ( x in the carrier of (ProjGroup (F,i)) implies x in rng f ) assume x in the carrier of (ProjGroup (F,i)) ; ::_thesis: x in rng f then consider g being Element of (F . i) such that A7: x = (1_ (product F)) +* (i,g) by Def1, A1; x = f . g by A7, A3; hence x in rng f by FUNCT_2:4; ::_thesis: verum end; then A8: the carrier of (ProjGroup (F,i)) c= rng f by TARSKI:def_3; rng f = the carrier of (ProjGroup (F,i)) by A8, XBOOLE_0:def_10; then A9: f is onto by FUNCT_2:def_3; for x1, x2 being set st x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 implies x1 = x2 ) assume A10: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 ) ; ::_thesis: x1 = x2 then reconsider xx1 = x1, xx2 = x2 as Element of the carrier of (F . i) ; A11: f . xx1 = (1_ (product F)) +* (i,xx1) by A3; A12: (1_ (product F)) +* (i,xx1) = (1_ (product F)) +* (i,xx2) by A10, A11, A3; the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; then A13: dom (1_ (product F)) = I by PARTFUN1:def_2; thus x1 = ((1_ (product F)) +* (i .--> xx1)) . i by FUNCT_7:94 .= ((1_ (product F)) +* (i,xx1)) . i by A13, FUNCT_7:def_3 .= ((1_ (product F)) +* (i .--> xx2)) . i by A13, A12, FUNCT_7:def_3 .= x2 by FUNCT_7:94 ; ::_thesis: verum end; then f is one-to-one by FUNCT_2:19; hence f is bijective by A9; ::_thesis: for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) thus for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) by A3; ::_thesis: verum end; definition let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; func 1ProdHom (F,i) -> Homomorphism of (F . i),(ProjGroup (F,i)) means :Def3: :: GROUP_12:def 3 for x being Element of (F . i) holds it . x = (1_ (product F)) +* (i,x); existence ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) proof ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1; hence ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ; ::_thesis: verum end; uniqueness for b1, b2 being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds b1 = b2 proof let F1, F2 be Homomorphism of (F . i),(ProjGroup (F,i)); ::_thesis: ( ( for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ) implies F1 = F2 ) assume that A1: for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) and A2: for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_Element_of_(F_._i)_holds_F1_._x_=_F2_._x let x be Element of (F . i); ::_thesis: F1 . x = F2 . x thus F1 . x = (1_ (product F)) +* (i,x) by A1 .= F2 . x by A2 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines 1ProdHom GROUP_12:def_3_:_ for I being non empty set for F being Group-like associative multMagma-Family of I for i being Element of I for b4 being Homomorphism of (F . i),(ProjGroup (F,i)) holds ( b4 = 1ProdHom (F,i) iff for x being Element of (F . i) holds b4 . x = (1_ (product F)) +* (i,x) ); registration let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; cluster 1ProdHom (F,i) -> bijective ; coherence 1ProdHom (F,i) is bijective proof consider f being Homomorphism of (F . i),(ProjGroup (F,i)) such that A1: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1; set F2 = 1ProdHom (F,i); for x being Element of (F . i) holds f . x = (1ProdHom (F,i)) . x by Def3, A1; hence 1ProdHom (F,i) is bijective by A1, FUNCT_2:63; ::_thesis: verum end; end; registration let I be non empty set ; let F be Group-like associative multMagma-Family of I; let i be Element of I; cluster ProjGroup (F,i) -> strict normal ; correctness coherence ProjGroup (F,i) is normal ; proof set H = ProjGroup (F,i); set G = product F; A1: for a being Element of (product F) holds (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) proof let a be Element of (product F); ::_thesis: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) now__::_thesis:_for_x_being_set_st_x_in_(a_*_(ProjGroup_(F,i)))_*_(a_")_holds_ x_in_the_carrier_of_(ProjGroup_(F,i)) let x be set ; ::_thesis: ( x in (a * (ProjGroup (F,i))) * (a ") implies x in the carrier of (ProjGroup (F,i)) ) assume x in (a * (ProjGroup (F,i))) * (a ") ; ::_thesis: x in the carrier of (ProjGroup (F,i)) then consider h being Element of (product F) such that A2: ( x = h * (a ") & h in a * (ProjGroup (F,i)) ) by GROUP_2:28; consider k being Element of (product F) such that A3: ( h = a * k & k in ProjGroup (F,i) ) by A2, GROUP_2:103; k in the carrier of (ProjGroup (F,i)) by A3, STRUCT_0:def_5; then k in ProjSet (F,i) by Def2; then consider m being Function, g being Element of (F . i) such that A4: ( m = k & dom m = I & m . i = g & ( for j being Element of I st j <> i holds m . j = 1_ (F . j) ) ) by Th2; set n = (a * k) * (a "); A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A6: dom (Carrier F) = I by PARTFUN1:def_2; A7: dom ((a * k) * (a ")) = I by A5, PARTFUN1:def_2; set Gi = F . i; consider Ri being 1-sorted such that A8: ( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def_13; set ak = a * k; set ad = a " ; reconsider xa = a . i, xk = k . i as Element of (F . i) by A8, A5, A6, CARD_3:9; A9: (a * k) . i = xa * xk by GROUP_7:1; A10: (a ") . i = xa " by GROUP_7:8; A11: ((a * k) * (a ")) . i = (xa * xk) * (xa ") by A9, A10, GROUP_7:1; now__::_thesis:_for_j_being_Element_of_I_st_j_<>_i_holds_ ((a_*_k)_*_(a_"))_._j_=_1__(F_._j) let j be Element of I; ::_thesis: ( j <> i implies ((a * k) * (a ")) . j = 1_ (F . j) ) assume j <> i ; ::_thesis: ((a * k) * (a ")) . j = 1_ (F . j) then A12: m . j = 1_ (F . j) by A4; set Gj = F . j; consider Rj being 1-sorted such that A13: ( Rj = F . j & (Carrier F) . j = the carrier of Rj ) by PRALG_1:def_13; reconsider xa = a . j, xk = k . j as Element of (F . j) by A13, A5, A6, CARD_3:9; A14: (a * k) . j = xa * xk by GROUP_7:1; A15: (a ") . j = xa " by GROUP_7:8; thus ((a * k) * (a ")) . j = (xa * xk) * (xa ") by A14, A15, GROUP_7:1 .= xa * (xa ") by A12, A4, GROUP_1:def_4 .= 1_ (F . j) by GROUP_1:def_5 ; ::_thesis: verum end; then (a * k) * (a ") in ProjSet (F,i) by A7, A11, Th2; hence x in the carrier of (ProjGroup (F,i)) by Def2, A2, A3; ::_thesis: verum end; hence (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by TARSKI:def_3; ::_thesis: verum end; A16: for a being Element of (product F) holds a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a proof let a be Element of (product F); ::_thesis: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a A17: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by A1; A18: (a ") * a = 1_ (product F) by GROUP_1:def_5; ((a * (ProjGroup (F,i))) * (a ")) * a = (a * ((ProjGroup (F,i)) * (a "))) * a by GROUP_2:106 .= a * (((ProjGroup (F,i)) * (a ")) * a) by GROUP_2:33 .= a * ((ProjGroup (F,i)) * ((a ") * a)) by GROUP_2:107 .= a * (ProjGroup (F,i)) by A18, GROUP_2:109 ; hence a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A17, GROUP_3:5; ::_thesis: verum end; A19: for a being Element of (product F) holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) proof let a be Element of (product F); ::_thesis: (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) A20: ((a ") * (ProjGroup (F,i))) * ((a ") ") c= the carrier of (ProjGroup (F,i)) by A1; A21: a * (a ") = 1_ (product F) by GROUP_1:def_5; a * (((a ") * (ProjGroup (F,i))) * a) = a * ((a ") * ((ProjGroup (F,i)) * a)) by GROUP_2:106 .= (a * (a ")) * ((ProjGroup (F,i)) * a) by GROUP_2:32 .= ((a * (a ")) * (ProjGroup (F,i))) * a by GROUP_2:106 .= (ProjGroup (F,i)) * a by A21, GROUP_2:109 ; hence (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A20, GROUP_3:5; ::_thesis: verum end; for a being Element of (product F) holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a proof let a be Element of (product F); ::_thesis: a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a A22: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A16; (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A19; hence a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a by A22, XBOOLE_0:def_10; ::_thesis: verum end; hence ProjGroup (F,i) is normal by GROUP_3:117; ::_thesis: verum end; end; theorem :: GROUP_12:7 for I being non empty set for F being Group-like associative multMagma-Family of I for i, j being Element of I for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds x * y = y * x proof let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I for i, j being Element of I for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds x * y = y * x let F be Group-like associative multMagma-Family of I; ::_thesis: for i, j being Element of I for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds x * y = y * x let i, j be Element of I; ::_thesis: for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds x * y = y * x set G = product F; let x, y be Element of (product F); ::_thesis: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) implies x * y = y * x ) assume A1: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) ) ; ::_thesis: x * y = y * x A2: ( the carrier of (ProjGroup (F,i)) = ProjSet (F,i) & the carrier of (ProjGroup (F,j)) = ProjSet (F,j) ) by Def2; A3: ( x in ProjSet (F,i) & y in ProjSet (F,j) ) by A2, A1, STRUCT_0:def_5; consider xx being Function, gx being Element of (F . i) such that A4: ( xx = x & dom xx = I & xx . i = gx & ( for k being Element of I st k <> i holds xx . k = 1_ (F . k) ) ) by A3, Th2; consider yy being Function, gy being Element of (F . j) such that A5: ( yy = y & dom yy = I & yy . j = gy & ( for k being Element of I st k <> j holds yy . k = 1_ (F . k) ) ) by A3, Th2; A6: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; set xy = x * y; set yx = y * x; A7: dom (x * y) = I by A6, PARTFUN1:def_2; A8: dom (y * x) = I by A6, PARTFUN1:def_2; for k being set st k in dom (x * y) holds (x * y) . k = (y * x) . k proof let k0 be set ; ::_thesis: ( k0 in dom (x * y) implies (x * y) . k0 = (y * x) . k0 ) assume k0 in dom (x * y) ; ::_thesis: (x * y) . k0 = (y * x) . k0 then reconsider k = k0 as Element of I by A6, PARTFUN1:def_2; percases ( ( k0 <> i & k0 <> j ) or k0 = i or k0 = j ) ; supposeA9: ( k0 <> i & k0 <> j ) ; ::_thesis: (x * y) . k0 = (y * x) . k0 then A10: xx . k = 1_ (F . k) by A4; A11: yy . k = 1_ (F . k) by A9, A5; (x * y) . k = (1_ (F . k)) * (1_ (F . k)) by A4, A5, A10, A11, GROUP_7:1 .= (y * x) . k by A4, A5, A10, A11, GROUP_7:1 ; hence (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum end; supposeA12: ( k0 = i or k0 = j ) ; ::_thesis: (x * y) . k0 = (y * x) . k0 percases ( k0 = i or k0 = j ) by A12; supposeA13: k0 = i ; ::_thesis: (x * y) . k0 = (y * x) . k0 then A14: yy . k = 1_ (F . k) by A1, A5; reconsider gx = gx as Element of (F . k) by A13; (x * y) . k = gx * (1_ (F . k)) by A4, A5, A14, A13, GROUP_7:1 .= gx by GROUP_1:def_4 .= (1_ (F . k)) * gx by GROUP_1:def_4 .= (y * x) . k by A4, A5, A14, A13, GROUP_7:1 ; hence (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum end; supposeA15: k0 = j ; ::_thesis: (x * y) . k0 = (y * x) . k0 then A16: xx . k = 1_ (F . k) by A1, A4; reconsider gy = gy as Element of (F . k) by A15; (x * y) . k = (1_ (F . k)) * gy by A4, A5, A16, A15, GROUP_7:1 .= gy by GROUP_1:def_4 .= gy * (1_ (F . k)) by GROUP_1:def_4 .= (y * x) . k by A4, A5, A16, A15, GROUP_7:1 ; hence (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum end; end; end; end; end; hence x * y = y * x by A7, A8, FUNCT_1:2; ::_thesis: verum end; theorem Th8: :: GROUP_12:8 for n being non empty Nat for F being Group-like associative multMagma-Family of Seg n for J being Nat for GJ being Group st 1 <= J & J <= n & GJ = F . J holds for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ proof let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n for J being Nat for GJ being Group st 1 <= J & J <= n & GJ = F . J holds for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for J being Nat for GJ being Group st 1 <= J & J <= n & GJ = F . J holds for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ let J be Nat; ::_thesis: for GJ being Group st 1 <= J & J <= n & GJ = F . J holds for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ let GJ be Group; ::_thesis: ( 1 <= J & J <= n & GJ = F . J implies for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ ) assume A1: ( 1 <= J & J <= n & GJ = F . J ) ; ::_thesis: for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ defpred S1[ Nat] means for x being Element of (product F) for s being FinSequence of (product F) st len s < J & len s = \$1 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ; A2: S1[ 0 ] proof let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ let s be FinSequence of (product F); ::_thesis: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ ) assume A3: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: x . J = 1_ GJ s = <*> the carrier of (product F) by A3; then A4: x = 1_ (product F) by A3, GROUP_4:8; J in Seg n by A1, FINSEQ_1:1; hence x . J = 1_ GJ by A1, A4, GROUP_7:6; ::_thesis: verum end; A5: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A6: S1[m] ; ::_thesis: S1[m + 1] let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ let s be FinSequence of (product F); ::_thesis: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ ) assume A7: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: x . J = 1_ GJ A8: m < m + 1 by NAT_1:13; A9: 1 <= len s by A7, NAT_1:11; ( 1 <= len s & len s <= n ) by A7, A1, NAT_1:11, XXREAL_0:2; then len s in Seg n ; then reconsider ls = len s as Element of Seg n ; set t = s | m; A10: now__::_thesis:_for_k_being_Element_of_Seg_n_st_k_in_dom_(s_|_m)_holds_ (s_|_m)_._k_in_ProjGroup_(F,k) let k be Element of Seg n; ::_thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) ) assume A11: k in dom (s | m) ; ::_thesis: (s | m) . k in ProjGroup (F,k) A12: (s | m) . k = s . k by A11, FUNCT_1:47; k in dom s by A11, RELAT_1:57; hence (s | m) . k in ProjGroup (F,k) by A12, A7; ::_thesis: verum end; set y = Product (s | m); dom s = Seg (m + 1) by A7, FINSEQ_1:def_3; then Seg m c= dom s by A8, FINSEQ_1:5; then A13: dom (s | m) = Seg m by RELAT_1:62; then A14: len (s | m) = m by FINSEQ_1:def_3; A15: len (s | m) = (len s) - 1 by A13, A7, FINSEQ_1:def_3; A16: (Product (s | m)) . J = 1_ GJ by A6, A10, A15, A7, XREAL_1:51; len s in Seg (len s) by A9; then A17: len s in dom s by FINSEQ_1:def_3; then reconsider sn = s . (len s) as Element of (product F) by FINSEQ_2:11; A18: (len (s | m)) + 1 = len s by A13, A7, FINSEQ_1:def_3; len ((s | m) ^ <*sn*>) = len s by A18, FINSEQ_2:16; then A19: dom ((s | m) ^ <*sn*>) = Seg (len s) by FINSEQ_1:def_3 .= dom s by FINSEQ_1:def_3 ; A20: s = (s | m) ^ <*sn*> proof for k being Nat st k in dom s holds s . k = ((s | m) ^ <*sn*>) . k proof let k be Nat; ::_thesis: ( k in dom s implies s . k = ((s | m) ^ <*sn*>) . k ) assume k in dom s ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k then A21: k in Seg ((len (s | m)) + 1) by A18, FINSEQ_1:def_3; now__::_thesis:_(_(_k_in_Seg_(len_(s_|_m))_&_s_._k_=_((s_|_m)_^_<*sn*>)_._k_)_or_(_k_=_(len_(s_|_m))_+_1_&_s_._k_=_((s_|_m)_^_<*sn*>)_._k_)_) percases ( k in Seg (len (s | m)) or k = (len (s | m)) + 1 ) by A21, FINSEQ_2:7; caseA22: k in Seg (len (s | m)) ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k then k in dom (s | m) by FINSEQ_1:def_3; then ((s | m) ^ <*sn*>) . k = (s | m) . k by FINSEQ_1:def_7 .= s . k by A22, A14, FUNCT_1:49 ; hence s . k = ((s | m) ^ <*sn*>) . k ; ::_thesis: verum end; case k = (len (s | m)) + 1 ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k hence s . k = ((s | m) ^ <*sn*>) . k by A18, FINSEQ_1:42; ::_thesis: verum end; end; end; hence s . k = ((s | m) ^ <*sn*>) . k ; ::_thesis: verum end; hence s = (s | m) ^ <*sn*> by A19, FINSEQ_1:13; ::_thesis: verum end; A23: x = (Product (s | m)) * sn by A20, A7, GROUP_4:6; s . (len s) in ProjGroup (F,ls) by A7, A17; then s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def_5; then A24: s . (len s) in ProjSet (F,ls) by Def2; consider snn being Function, gn being Element of (F . ls) such that A25: ( snn = sn & dom snn = Seg n & snn . ls = gn & ( for k being Element of Seg n st k <> ls holds snn . k = 1_ (F . k) ) ) by A24, Th2; thus x . J = 1_ GJ ::_thesis: verum proof reconsider J0 = J as Element of Seg n by A1, FINSEQ_1:1; A26: snn . J0 = 1_ (F . J0) by A25, A7; thus x . J = (1_ (F . J0)) * (1_ (F . J0)) by A16, A25, A26, A23, A1, GROUP_7:1 .= 1_ GJ by A1, GROUP_1:def_4 ; ::_thesis: verum end; end; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A2, A5); hence for x being Element of (product F) for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds x . J = 1_ GJ ; ::_thesis: verum end; theorem Th9: :: GROUP_12:9 for n being non empty Nat for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) proof let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F) for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) defpred S1[ Nat] means for x being Element of (product F) for s being FinSequence of (product F) st 1 <= len s & len s <= \$1 & \$1 <= n & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ); A1: S1[ 0 ] ; A2: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A3: S1[m] ; ::_thesis: S1[m + 1] let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) let s be FinSequence of (product F); ::_thesis: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ) assume A4: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) then A5: len s = 1 by A4, XXREAL_0:1; then A6: s = <*(s . 1)*> by FINSEQ_1:40; thus for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i <= len s implies ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ) assume A7: ( 1 <= i & i <= len s ) ; ::_thesis: ex si being Element of (product F) st ( si = s . i & x . i = si . i ) 1 in Seg (len s) by A4; then 1 in dom s by FINSEQ_1:def_3; then reconsider si = s . 1 as Element of (product F) by FINSEQ_2:11; take si ; ::_thesis: ( si = s . i & x . i = si . i ) thus ( si = s . i & x . i = si . i ) by A7, A6, A4, A5, GROUP_4:9, XXREAL_0:1; ::_thesis: verum end; end; supposeA8: m <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_ ex_si_being_Element_of_(product_F)_st_ (_si_=_s_._i_&_x_._i_=_si_._i_) percases ( len s <= m or len s > m ) ; supposeA9: len s <= m ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ( 1 <= len s & len s <= m & m <= n ) proof (m + 1) - 1 <= n - 0 by A4, XREAL_1:13; hence ( 1 <= len s & len s <= m & m <= n ) by A4, A9; ::_thesis: verum end; hence for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) by A3, A4; ::_thesis: verum end; supposeA10: len s > m ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) A11: len s = m + 1 by A4, A10, NAT_1:8; A12: len s <= n by A4, A10, NAT_1:8; then len s in Seg n by A4; then reconsider ls = len s as Element of Seg n ; set t = s | m; A13: m < m + 1 by NAT_1:13; dom s = Seg (m + 1) by A11, FINSEQ_1:def_3; then Seg m c= dom s by A13, FINSEQ_1:5; then dom (s | m) = Seg m by RELAT_1:62; then A14: len (s | m) = m by FINSEQ_1:def_3; A15: 0 + 1 <= m by A8, NAT_1:13; A16: (m + 1) - 1 <= n - 0 by A4, XREAL_1:13; A17: ( dom s = Seg (len s) & dom (s | m) = Seg (len (s | m)) ) by FINSEQ_1:def_3; A18: now__::_thesis:_for_k_being_Element_of_Seg_n_st_k_in_dom_(s_|_m)_holds_ (s_|_m)_._k_in_ProjGroup_(F,k) let k be Element of Seg n; ::_thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) ) assume A19: k in dom (s | m) ; ::_thesis: (s | m) . k in ProjGroup (F,k) then A20: (s | m) . k = s . k by FUNCT_1:47; Seg (len (s | m)) c= Seg (len s) by A14, A10, FINSEQ_1:5; hence (s | m) . k in ProjGroup (F,k) by A20, A4, A19, A17; ::_thesis: verum end; set y = Product (s | m); A21: len s in Seg (len s) by A4; then reconsider sn = s . (len s) as Element of (product F) by A17, FINSEQ_2:11; A22: s = (s | m) ^ <*sn*> by A11, FINSEQ_3:55; A23: x = (Product (s | m)) * sn by A22, A4, GROUP_4:6; s . (len s) in ProjGroup (F,ls) by A17, A4, A21; then s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def_5; then A24: s . (len s) in ProjSet (F,ls) by Def2; set Gn = F . ls; consider snn being Function, gn being Element of (F . ls) such that A25: ( snn = sn & dom snn = Seg n & snn . ls = gn & ( for k being Element of Seg n st k <> ls holds snn . k = 1_ (F . k) ) ) by A24, Th2; thus for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i <= len s implies ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ) assume A26: ( 1 <= i & i <= len s ) ; ::_thesis: ex si being Element of (product F) st ( si = s . i & x . i = si . i ) percases ( i <> len s or i = len s ) ; supposeA27: i <> len s ; ::_thesis: ex si being Element of (product F) st ( si = s . i & x . i = si . i ) then A28: i < len s by A26, XXREAL_0:1; len s = (len (s | m)) + (len <*sn*>) by A22, FINSEQ_1:22 .= (len (s | m)) + 1 by FINSEQ_1:40 ; then A29: ( 1 <= i & i <= len (s | m) ) by A26, A28, NAT_1:13; then consider ti being Element of (product F) such that A30: ( ti = (s | m) . i & (Product (s | m)) . i = ti . i ) by A3, A16, A18, A14, A15; A31: (s | m) . i = s . i by A29, A22, FINSEQ_1:64; ( 1 <= i & i <= n ) by A29, A16, A14, XXREAL_0:2; then reconsider ii = i as Element of Seg n by FINSEQ_1:1; A32: sn . ii = 1_ (F . ii) by A25, A27; consider Rii being 1-sorted such that A33: ( Rii = F . ii & (Carrier F) . ii = the carrier of Rii ) by PRALG_1:def_13; A34: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A35: dom (Carrier F) = Seg n by PARTFUN1:def_2; reconsider tii = ti . i as Element of (F . ii) by A33, A34, A35, CARD_3:9; x . i = tii * (1_ (F . ii)) by A30, A32, A23, GROUP_7:1 .= ti . i by GROUP_1:def_4 ; hence ex si being Element of (product F) st ( si = s . i & x . i = si . i ) by A30, A31; ::_thesis: verum end; supposeA36: i = len s ; ::_thesis: ex si being Element of (product F) st ( si = s . i & x . i = si . i ) A37: (Product (s | m)) . i = 1_ (F . ls) by A36, Th8, A18, A10, A14, A12, A26; x . i = (1_ (F . ls)) * gn by A36, A37, A25, A23, GROUP_7:1 .= sn . i by A25, A36, GROUP_1:def_4 ; hence ex si being Element of (product F) st ( si = s . i & x . i = si . i ) by A36; ::_thesis: verum end; end; end; end; end; end; hence for i being Nat st 1 <= i & i <= len s holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ; ::_thesis: verum end; end; end; A38: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A1, A2); thus for x being Element of (product F) for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ::_thesis: verum proof let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) let s be FinSequence of (product F); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) ) assume A39: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) A40: ( 1 <= len s & len s <= n ) by A39, NAT_1:14; for k being Element of Seg n st k in dom s holds s . k in ProjGroup (F,k) by A39; hence for i being Nat st 1 <= i & i <= n holds ex si being Element of (product F) st ( si = s . i & x . i = si . i ) by A39, A40, A38; ::_thesis: verum end; end; theorem Th10: :: GROUP_12:10 for n being non empty Nat for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds s = t proof let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds s = t let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F) for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds s = t let x be Element of (product F); ::_thesis: for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds s = t let s, t be FinSequence of (product F); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t implies s = t ) set I = Seg n; assume that A1: len s = n and A2: for k being Element of Seg n holds s . k in ProjGroup (F,k) and A3: x = Product s and A4: len t = n and A5: for k being Element of Seg n holds t . k in ProjGroup (F,k) and A6: x = Product t ; ::_thesis: s = t now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_ s_._i_=_t_._i let i be Nat; ::_thesis: ( 1 <= i & i <= n implies s . i = t . i ) assume A7: ( 1 <= i & i <= n ) ; ::_thesis: s . i = t . i then reconsider i0 = i as Element of Seg n by FINSEQ_1:1; consider si being Element of (product F) such that A8: ( si = s . i & x . i = si . i ) by A1, A2, A3, A7, Th9; consider ti being Element of (product F) such that A9: ( ti = t . i & x . i = ti . i ) by A4, A5, A6, A7, Th9; s . i0 in ProjGroup (F,i0) by A2; then s . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def_5; then A10: s . i0 in ProjSet (F,i0) by Def2; consider sn being Function, gn being Element of (F . i0) such that A11: ( sn = si & dom sn = Seg n & sn . i0 = gn & ( for k being Element of Seg n st k <> i0 holds sn . k = 1_ (F . k) ) ) by A8, A10, Th2; t . i0 in ProjGroup (F,i0) by A5; then t . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def_5; then A12: t . i0 in ProjSet (F,i0) by Def2; consider tn being Function, fn being Element of (F . i0) such that A13: ( tn = ti & dom tn = Seg n & tn . i0 = fn & ( for k being Element of Seg n st k <> i0 holds tn . k = 1_ (F . k) ) ) by A9, A12, Th2; now__::_thesis:_for_x_being_set_st_x_in_dom_sn_holds_ sn_._x_=_tn_._x let x be set ; ::_thesis: ( x in dom sn implies sn . b1 = tn . b1 ) assume x in dom sn ; ::_thesis: sn . b1 = tn . b1 then reconsider j = x as Element of Seg n by A11; percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: sn . b1 = tn . b1 hence sn . x = tn . x by A8, A9, A11, A13; ::_thesis: verum end; supposeA14: j <> i ; ::_thesis: sn . b1 = tn . b1 then sn . j = 1_ (F . j) by A11; hence sn . x = tn . x by A14, A13; ::_thesis: verum end; end; end; hence s . i = t . i by A8, A9, A11, A13, FUNCT_1:2; ::_thesis: verum end; hence s = t by A1, A4, FINSEQ_1:14; ::_thesis: verum end; theorem Th11: :: GROUP_12:11 for n being non empty Nat for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) ex s being FinSequence of (product F) st ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) proof let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n for x being Element of (product F) ex s being FinSequence of (product F) st ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F) ex s being FinSequence of (product F) st ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) let x be Element of (product F); ::_thesis: ex s being FinSequence of (product F) st ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) set I = Seg n; defpred S1[ Nat, set ] means ex k being Element of Seg n ex g being Element of (F . k) st ( k = \$1 & x . k = g & \$2 = (1_ (product F)) +* (k,g) ); A1: for k being Nat st k in Seg n holds ex z being Element of (product F) st S1[k,z] proof let k be Nat; ::_thesis: ( k in Seg n implies ex z being Element of (product F) st S1[k,z] ) assume k in Seg n ; ::_thesis: ex z being Element of (product F) st S1[k,z] then reconsider k0 = k as Element of Seg n ; A2: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A3: dom (Carrier F) = Seg n by PARTFUN1:def_2; consider Rj being 1-sorted such that A4: ( Rj = F . k0 & (Carrier F) . k0 = the carrier of Rj ) by PRALG_1:def_13; reconsider g = x . k0 as Element of (F . k0) by A4, A3, A2, CARD_3:9; (1_ (product F)) +* (k0,g) in ProjSet (F,k0) by Def1; then reconsider z = (1_ (product F)) +* (k0,g) as Element of (product F) ; take z ; ::_thesis: S1[k,z] thus S1[k,z] ; ::_thesis: verum end; consider s being FinSequence of (product F) such that A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds S1[k,s . k] ) ) from FINSEQ_1:sch_5(A1); take s ; ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) n in NAT by ORDINAL1:def_12; hence A6: len s = n by A5, FINSEQ_1:def_3; ::_thesis: ( ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) thus A7: for k being Element of Seg n holds s . k in ProjGroup (F,k) ::_thesis: x = Product s proof let k be Element of Seg n; ::_thesis: s . k in ProjGroup (F,k) ex k0 being Element of Seg n ex g being Element of (F . k0) st ( k0 = k & x . k0 = g & s . k = (1_ (product F)) +* (k0,g) ) by A5; then A8: s . k in ProjSet (F,k) by Def1; the carrier of (ProjGroup (F,k)) = ProjSet (F,k) by Def2; hence s . k in ProjGroup (F,k) by A8, STRUCT_0:def_5; ::_thesis: verum end; set y = Product s; A9: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A10: dom x = Seg n by A9, PARTFUN1:def_2; A11: dom (Product s) = Seg n by A9, PARTFUN1:def_2; A12: dom (1_ (product F)) = Seg n by A9, PARTFUN1:def_2; now__::_thesis:_for_t_being_set_st_t_in_dom_x_holds_ x_._t_=_(Product_s)_._t let t be set ; ::_thesis: ( t in dom x implies x . t = (Product s) . t ) assume t in dom x ; ::_thesis: x . t = (Product s) . t then A13: t in Seg n by A9, PARTFUN1:def_2; then reconsider i = t as Nat ; ( 1 <= i & i <= n ) by A13, FINSEQ_1:1; then A14: ex si being Element of (product F) st ( si = s . i & (Product s) . i = si . i ) by Th9, A6, A7; ex i1 being Element of Seg n ex g being Element of (F . i1) st ( i1 = i & x . i1 = g & s . i = (1_ (product F)) +* (i1,g) ) by A13, A5; hence x . t = (Product s) . t by A12, A14, FUNCT_7:31; ::_thesis: verum end; hence x = Product s by A10, A11, FUNCT_1:2; ::_thesis: verum end; theorem Th12: :: GROUP_12:12 for n being non empty Nat for G being commutative Group for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t ) holds ex f being Homomorphism of (product F),G st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) proof let n be non empty Nat; ::_thesis: for G being commutative Group for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t ) holds ex f being Homomorphism of (product F),G st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) let G be commutative Group; ::_thesis: for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t ) holds ex f being Homomorphism of (product F),G st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) let F be Group-like associative multMagma-Family of Seg n; ::_thesis: ( ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t ) implies ex f being Homomorphism of (product F),G st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) ) set I = Seg n; assume that A1: for i being Element of Seg n holds F . i is Subgroup of G and A2: for x being Element of G ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) and A3: for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t ; ::_thesis: ex f being Homomorphism of (product F),G st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) A4: for x being Element of (product F) holds ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds x . i in (Carrier F) . i ) ) proof let x be Element of (product F); ::_thesis: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds x . i in (Carrier F) . i ) ) A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A6: dom (Carrier F) = Seg n by PARTFUN1:def_2; dom x = Seg n by A5, PARTFUN1:def_2; then reconsider s = x as FinSequence by FINSEQ_1:def_2; A7: for i being Element of Seg n holds x . i in the carrier of (F . i) proof let i be Element of Seg n; ::_thesis: x . i in the carrier of (F . i) ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; hence x . i in the carrier of (F . i) by A6, A5, CARD_3:9; ::_thesis: verum end; for i being Nat st i in dom s holds s . i in the carrier of G proof let i be Nat; ::_thesis: ( i in dom s implies s . i in the carrier of G ) assume i in dom s ; ::_thesis: s . i in the carrier of G then reconsider j = i as Element of Seg n by A5, PARTFUN1:def_2; A8: s . j in the carrier of (F . j) by A7; F . j is Subgroup of G by A1; then the carrier of (F . j) c= the carrier of G by GROUP_2:def_5; hence s . i in the carrier of G by A8; ::_thesis: verum end; hence ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds x . i in (Carrier F) . i ) ) by A5, CARD_3:9, FINSEQ_2:12, PARTFUN1:def_2; ::_thesis: verum end; defpred S1[ set , set ] means ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = \$1 & \$2 = Product s ); A9: for x being Element of (product F) ex y being Element of G st S1[x,y] proof let x be Element of (product F); ::_thesis: ex y being Element of G st S1[x,y] A10: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds x . i in (Carrier F) . i ) ) by A4; reconsider s = x as FinSequence of G by A4; A11: dom x = Seg n by A4; A12: for i being Element of Seg n holds x . i in the carrier of (F . i) proof let i be Element of Seg n; ::_thesis: x . i in the carrier of (F . i) ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; hence x . i in the carrier of (F . i) by A10; ::_thesis: verum end; n in NAT by ORDINAL1:def_12; then A13: len s = n by A11, FINSEQ_1:def_3; A14: now__::_thesis:_for_k_being_Element_of_Seg_n_holds_s_._k_in_F_._k let k be Element of Seg n; ::_thesis: s . k in F . k s . k in the carrier of (F . k) by A12; hence s . k in F . k by STRUCT_0:def_5; ::_thesis: verum end; take Product s ; ::_thesis: S1[x, Product s] thus S1[x, Product s] by A13, A14; ::_thesis: verum end; consider f being Function of (product F),G such that A15: for x being Element of the carrier of (product F) holds S1[x,f . x] from FUNCT_2:sch_3(A9); for a, b being Element of (product F) holds f . (a * b) = (f . a) * (f . b) proof let a, b be Element of (product F); ::_thesis: f . (a * b) = (f . a) * (f . b) A16: ( a is FinSequence of G & dom a = Seg n & dom a = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds a . i in (Carrier F) . i ) ) by A4; reconsider a1 = a as FinSequence of G by A4; A17: ( b is FinSequence of G & dom b = Seg n & dom b = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds b . i in (Carrier F) . i ) ) by A4; reconsider b1 = b as FinSequence of G by A4; reconsider ab1 = a * b as FinSequence of G by A4; A18: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_ab1_holds_ ab1_._k_=_(a1_/._k)_*_(b1_/._k) let k be Element of NAT ; ::_thesis: ( k in dom ab1 implies ab1 . k = (a1 /. k) * (b1 /. k) ) assume k in dom ab1 ; ::_thesis: ab1 . k = (a1 /. k) * (b1 /. k) then reconsider k0 = k as Element of Seg n by A4; ex R being 1-sorted st ( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def_13; then reconsider aa = a . k0 as Element of (F . k0) by A16; ex R being 1-sorted st ( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def_13; then reconsider bb = b . k0 as Element of (F . k0) by A17; A19: aa = a1 /. k0 by A16, PARTFUN1:def_6; A20: bb = b1 /. k0 by A17, PARTFUN1:def_6; A21: F . k0 is Subgroup of G by A1; thus ab1 . k = aa * bb by GROUP_7:1 .= (a1 /. k) * (b1 /. k) by A19, A20, A21, GROUP_2:43 ; ::_thesis: verum end; A22: ex sa being FinSequence of G st ( len sa = n & ( for k being Element of Seg n holds sa . k in F . k ) & sa = a & f . a = Product sa ) by A15; A23: ex sb being FinSequence of G st ( len sb = n & ( for k being Element of Seg n holds sb . k in F . k ) & sb = b & f . b = Product sb ) by A15; ex sab being FinSequence of G st ( len sab = n & ( for k being Element of Seg n holds sab . k in F . k ) & sab = a * b & f . (a * b) = Product sab ) by A15; hence f . (a * b) = (f . a) * (f . b) by A18, A22, A23, GROUP_4:17; ::_thesis: verum end; then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def_6; take f ; ::_thesis: ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_ y_in_rng_f let y be set ; ::_thesis: ( y in the carrier of G implies y in rng f ) assume y in the carrier of G ; ::_thesis: y in rng f then consider s being FinSequence of G such that A24: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & y = Product s ) by A2; A25: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2; A26: dom s = Seg n by A24, FINSEQ_1:def_3; A27: dom (Carrier F) = Seg n by PARTFUN1:def_2; A28: for x being set st x in dom (Carrier F) holds s . x in (Carrier F) . x proof let x be set ; ::_thesis: ( x in dom (Carrier F) implies s . x in (Carrier F) . x ) assume x in dom (Carrier F) ; ::_thesis: s . x in (Carrier F) . x then reconsider i = x as Element of Seg n ; A29: s . i in F . i by A24; ex R being 1-sorted st ( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13; hence s . x in (Carrier F) . x by A29, STRUCT_0:def_5; ::_thesis: verum end; reconsider x = s as Element of (product F) by A25, A26, A27, A28, CARD_3:9; ex t being FinSequence of G st ( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x & f . x = Product t ) by A15; hence y in rng f by A24, FUNCT_2:4; ::_thesis: verum end; then A30: the carrier of G c= rng f by TARSKI:def_3; rng f = the carrier of G by A30, XBOOLE_0:def_10; then A31: f is onto by FUNCT_2:def_3; for x1, x2 being set st x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 implies x1 = x2 ) assume A32: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 ) ; ::_thesis: x1 = x2 consider s being FinSequence of G such that A33: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x1 & f . x1 = Product s ) by A15, A32; consider t being FinSequence of G such that A34: ( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x2 & f . x2 = Product t ) by A15, A32; thus x1 = x2 by A3, A33, A32, A34; ::_thesis: verum end; then f is one-to-one by FUNCT_2:19; hence ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) by A15, A31; ::_thesis: verum end; theorem :: GROUP_12:13 for n being non empty Nat for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds ex f being Homomorphism of (product F),(product G) st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) proof let n be non empty Nat; ::_thesis: for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds ex f being Homomorphism of (product F),(product G) st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) let G, F be Group-like associative commutative multMagma-Family of Seg n; ::_thesis: ( ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) implies ex f being Homomorphism of (product F),(product G) st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) ) assume A1: for k being Element of Seg n holds F . k = ProjGroup (G,k) ; ::_thesis: ex f being Homomorphism of (product F),(product G) st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) A2: for i being Element of Seg n holds F . i is Subgroup of product G proof let i be Element of Seg n; ::_thesis: F . i is Subgroup of product G F . i = ProjGroup (G,i) by A1; hence F . i is Subgroup of product G ; ::_thesis: verum end; A3: for x being Element of (product G) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) proof let x be Element of (product G); ::_thesis: ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) consider s being FinSequence of (product G) such that A4: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (G,k) ) & x = Product s ) by Th11; take s ; ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) for k being Element of Seg n holds s . k in F . k proof let k be Element of Seg n; ::_thesis: s . k in F . k s . k in ProjGroup (G,k) by A4; hence s . k in F . k by A1; ::_thesis: verum end; hence ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) by A4; ::_thesis: verum end; for s, t being FinSequence of (product G) st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds s = t proof let s, t be FinSequence of (product G); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t implies s = t ) assume A5: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t ) ; ::_thesis: s = t for k being Element of Seg n holds ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) proof let k be Element of Seg n; ::_thesis: ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) ( s . k in F . k & t . k in F . k ) by A5; hence ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) by A1; ::_thesis: verum end; hence s = t by A5, Th10; ::_thesis: verum end; hence ex f being Homomorphism of (product F),(product G) st ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) by A2, A3, Th12; ::_thesis: verum end;