:: FINSOP_1 semantic presentation begin definition let D be non empty set ; let F be FinSequence of D; let g be BinOp of D; assume A1: ( g is having_a_unity or len F >= 1 ) ; funcg "**" F -> Element of D means :Def1: :: FINSOP_1:def 1 it = the_unity_wrt g if ( g is having_a_unity & len F = 0 ) otherwise ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & it = f . (len F) ); existence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) proof now__::_thesis:_(_(_g_is_having_a_unity_&_len_F_=_0_implies_ex_b1_being_Element_of_D_st_b1_=_the_unity_wrt_g_)_&_(_(_not_g_is_having_a_unity_or_not_len_F_=_0_)_implies_ex_b1_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_ (_f_._1_=_F_._1_&_(_for_n_being_Element_of_NAT_st_0_<>_n_&_n_<_len_F_holds_ f_._(n_+_1)_=_g_._((f_._n),(F_._(n_+_1)))_)_&_b1_=_f_._(len_F)_)_)_) percases ( len F = 0 or len F <> 0 ) ; suppose len F = 0 ; ::_thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A1; ::_thesis: verum end; supposeA2: len F <> 0 ; ::_thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) defpred S1[ Element of NAT ] means for F being FinSequence of D st len F = \$1 & len F <> 0 holds ex d being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] let F be FinSequence of D; ::_thesis: ( len F = k + 1 & len F <> 0 implies ex d being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) ) assume that A5: len F = k + 1 and len F <> 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) reconsider G = F | (Seg k) as FinSequence of D by FINSEQ_1:18; A6: len G = k by A5, FINSEQ_3:53; now__::_thesis:_ex_d_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_ (_f_._1_=_F_._1_&_(_for_n_being_Element_of_NAT_st_0_<>_n_&_n_<_len_F_holds_ f_._(n_+_1)_=_g_._((f_._n),(F_._(n_+_1)))_)_&_d_=_f_._(len_F)_) percases ( len G = 0 or len G <> 0 ) ; supposeA7: len G = 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) set f = NAT --> (F . 1); A8: rng (NAT --> (F . 1)) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (NAT --> (F . 1)) or x in D ) assume x in rng (NAT --> (F . 1)) ; ::_thesis: x in D then ex y being set st ( y in dom (NAT --> (F . 1)) & (NAT --> (F . 1)) . y = x ) by FUNCT_1:def_3; then A9: x = F . 1 by FUNCOP_1:7; 1 in dom F by A5, A6, A7, FINSEQ_3:25; then A10: x in rng F by A9, FUNCT_1:def_3; rng F c= D by FINSEQ_1:def_4; hence x in D by A10; ::_thesis: verum end; dom (NAT --> (F . 1)) = NAT by FUNCOP_1:13; then reconsider f = NAT --> (F . 1) as Function of NAT,D by A8, RELSET_1:4; take d = f . 1; ::_thesis: ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) take f = f; ::_thesis: ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) thus f . 1 = F . 1 by FUNCOP_1:7; ::_thesis: ( ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) thus for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) by A5, A6, A7, NAT_1:14; ::_thesis: d = f . (len F) thus d = f . (len F) by A5, A6, A7; ::_thesis: verum end; supposeA11: len G <> 0 ; ::_thesis: ex a being Element of D ex h being Function of NAT,D st ( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) ) reconsider j = len F as Element of NAT ; 1 <= len F by A5, NAT_1:12; then len F in dom F by FINSEQ_3:25; then A12: F . (len F) in rng F by FUNCT_1:def_3; rng F c= D by FINSEQ_1:def_4; then reconsider t = F . (len F) as Element of D by A12; len G >= 1 by A11, NAT_1:14; then A13: 1 in dom G by FINSEQ_3:25; consider d being Element of D, f being Function of NAT,D such that A14: f . 1 = G . 1 and A15: for n being Element of NAT st 0 <> n & n < len G holds f . (n + 1) = g . ((f . n),(G . (n + 1))) and A16: d = f . (len G) by A4, A5, A11, FINSEQ_3:53; deffunc H1( Element of NAT ) -> Element of D = f . \$1; consider h being Function of NAT,D such that A17: h . j = g . (d,t) and A18: for n being Element of NAT st n <> j holds h . n = H1(n) from FUNCT_2:sch_6(); take a = h . j; ::_thesis: ex h being Function of NAT,D st ( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) ) take h = h; ::_thesis: ( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) ) 1 <> j by A5, A11, FINSEQ_3:53; hence h . 1 = G . 1 by A14, A18 .= F . 1 by A13, FUNCT_1:47 ; ::_thesis: ( ( for n being Element of NAT st 0 <> n & n < len F holds h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) ) thus for n being Element of NAT st 0 <> n & n < len F holds h . (n + 1) = g . ((h . n),(F . (n + 1))) ::_thesis: a = h . (len F) proof let n be Element of NAT ; ::_thesis: ( 0 <> n & n < len F implies h . (n + 1) = g . ((h . n),(F . (n + 1))) ) assume that A19: n <> 0 and A20: n < len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1))) now__::_thesis:_h_._(n_+_1)_=_g_._((h_._n),(F_._(n_+_1))) percases ( n + 1 = len F or n + 1 <> len F ) ; supposeA21: n + 1 = len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1))) len G <> len F by A5, A6; hence h . (n + 1) = g . ((h . n),(F . (n + 1))) by A5, A6, A16, A17, A18, A21; ::_thesis: verum end; supposeA22: n + 1 <> len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1))) n + 1 <= len F by A20, NAT_1:13; then A23: n + 1 < len F by A22, XXREAL_0:1; then A24: n < len G by A5, A6, XREAL_1:6; ( 1 <= n + 1 & n + 1 <= len G ) by A5, A6, A23, NAT_1:12, NAT_1:13; then A25: n + 1 in dom G by FINSEQ_3:25; h . (n + 1) = f . (n + 1) by A18, A22 .= g . ((f . n),(G . (n + 1))) by A15, A19, A24 .= g . ((f . n),(F . (n + 1))) by A25, FUNCT_1:47 .= g . ((h . n),(F . (n + 1))) by A18, A20 ; hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; ::_thesis: verum end; end; end; hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; ::_thesis: verum end; thus a = h . (len F) ; ::_thesis: verum end; end; end; hence ex d being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) ; ::_thesis: verum end; A26: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A3); hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A2; ::_thesis: verum end; end; end; hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of D holds ( ( g is having_a_unity & len F = 0 & b1 = the_unity_wrt g & b2 = the_unity_wrt g implies b1 = b2 ) & ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b2 = f . (len F) ) implies b1 = b2 ) ) proof let d1, d2 be Element of D; ::_thesis: ( ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) & ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 ) ) thus ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) ; ::_thesis: ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 ) assume A27: ( not g is having_a_unity or len F <> 0 ) ; ::_thesis: ( for f being Function of NAT,D holds ( not f . 1 = F . 1 or ex n being Element of NAT st ( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d1 = f . (len F) ) or for f being Function of NAT,D holds ( not f . 1 = F . 1 or ex n being Element of NAT st ( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 ) given f1 being Function of NAT,D such that A28: f1 . 1 = F . 1 and A29: for n being Element of NAT st 0 <> n & n < len F holds f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) and A30: d1 = f1 . (len F) ; ::_thesis: ( for f being Function of NAT,D holds ( not f . 1 = F . 1 or ex n being Element of NAT st ( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 ) given f2 being Function of NAT,D such that A31: f2 . 1 = F . 1 and A32: for n being Element of NAT st 0 <> n & n < len F holds f2 . (n + 1) = g . ((f2 . n),(F . (n + 1))) and A33: d2 = f2 . (len F) ; ::_thesis: d1 = d2 defpred S1[ Element of NAT ] means ( \$1 <> 0 & \$1 <= len F implies f1 . \$1 = f2 . \$1 ); A34: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A35: ( n <> 0 & n <= len F implies f1 . n = f2 . n ) ; ::_thesis: S1[n + 1] assume that n + 1 <> 0 and A36: n + 1 <= len F ; ::_thesis: f1 . (n + 1) = f2 . (n + 1) now__::_thesis:_f1_._(n_+_1)_=_f2_._(n_+_1) percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: f1 . (n + 1) = f2 . (n + 1) hence f1 . (n + 1) = f2 . (n + 1) by A28, A31; ::_thesis: verum end; supposeA37: n <> 0 ; ::_thesis: f1 . (n + 1) = f2 . (n + 1) A38: n < len F by A36, NAT_1:13; then f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) by A29, A37; hence f1 . (n + 1) = f2 . (n + 1) by A32, A35, A37, A38; ::_thesis: verum end; end; end; hence f1 . (n + 1) = f2 . (n + 1) ; ::_thesis: verum end; A39: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A39, A34); hence d1 = d2 by A1, A27, A30, A33; ::_thesis: verum end; consistency for b1 being Element of D holds verum ; end; :: deftheorem Def1 defines "**" FINSOP_1:def_1_:_ for D being non empty set for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds for b4 being Element of D holds ( ( g is having_a_unity & len F = 0 implies ( b4 = g "**" F iff b4 = the_unity_wrt g ) ) & ( ( not g is having_a_unity or not len F = 0 ) implies ( b4 = g "**" F iff ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b4 = f . (len F) ) ) ) ); theorem :: FINSOP_1:1 for D being non empty set for F being FinSequence of D for g being BinOp of D st len F >= 1 holds ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & g "**" F = f . (len F) ) by Def1; theorem :: FINSOP_1:2 for D being non empty set for d being Element of D for F being FinSequence of D for g being BinOp of D st len F >= 1 & ex f being Function of NAT,D st ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) holds d = g "**" F by Def1; definition let A be non empty set ; let F be Function of NAT,A; let p be FinSequence of A; :: original: +* redefine funcF +* p -> Function of NAT,A; coherence F +* p is Function of NAT,A proof A1: dom F = NAT by FUNCT_2:def_1; dom (F +* p) = (dom F) \/ (dom p) by FUNCT_4:def_1 .= NAT by A1, XBOOLE_1:12 ; hence F +* p is Function of NAT,A by FUNCT_2:def_1; ::_thesis: verum end; end; notation let f be FinSequence; synonym findom f for dom f; end; definition let f be FinSequence; :: original: findom redefine func findom f -> Element of Fin NAT; coherence findom f is Element of Fin NAT proof dom f = Seg (len f) by FINSEQ_1:def_3; hence findom f is Element of Fin NAT by FINSUB_1:def_5; ::_thesis: verum end; end; Lm1: for D being non empty set for F being FinSequence of D for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) proof let D be non empty set ; ::_thesis: for F being FinSequence of D for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let g be BinOp of D; ::_thesis: ( len F >= 1 & g is associative & g is commutative implies g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) ) assume that A1: len F >= 1 and A2: ( g is associative & g is commutative ) ; ::_thesis: g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) set A = findom F; set h = (NAT --> (the_unity_wrt g)) +* F; A3: dom F = Seg (len F) by FINSEQ_1:def_3; then consider G being Function of (Fin NAT),D such that A4: g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) = G . (findom F) and for d being Element of D st d is_a_unity_wrt g holds G . {} = d and A5: for n being Element of NAT holds G . {n} = ((NAT --> (the_unity_wrt g)) +* F) . n and A6: for B being Element of Fin NAT st B c= findom F & B <> {} holds for n being Element of NAT st n in (findom F) \ B holds G . (B \/ {n}) = g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . n)) by A1, A2, SETWISEO:def_3; consider f being Function of NAT,D such that A7: f . 1 = F . 1 and A8: for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) and A9: g "**" F = f . (len F) by A1, Def1; defpred S1[ Element of NAT ] means ( \$1 <> 0 & \$1 <= len F implies f . \$1 = G . (Seg \$1) ); A10: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A11: ( n <> 0 & n <= len F implies f . n = G . (Seg n) ) ; ::_thesis: S1[n + 1] assume that n + 1 <> 0 and A12: n + 1 <= len F ; ::_thesis: f . (n + 1) = G . (Seg (n + 1)) now__::_thesis:_f_._(n_+_1)_=_G_._(Seg_(n_+_1)) percases ( n = 0 or n <> 0 ) ; supposeA13: n = 0 ; ::_thesis: f . (n + 1) = G . (Seg (n + 1)) 1 in dom F by A1, A3, FINSEQ_1:1; then ((NAT --> (the_unity_wrt g)) +* F) . 1 = F . 1 by FUNCT_4:13; hence f . (n + 1) = G . (Seg (n + 1)) by A7, A5, A13, FINSEQ_1:2; ::_thesis: verum end; supposeA14: n <> 0 ; ::_thesis: f . (n + 1) = G . (Seg (n + 1)) reconsider B = Seg n as Element of Fin NAT by FINSUB_1:def_5; n + 1 >= 1 by NAT_1:12; then A15: n + 1 in dom F by A12, FINSEQ_3:25; A16: n < len F by A12, NAT_1:13; then A17: f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A14; not n + 1 in Seg n by FINSEQ_3:10; then A18: n + 1 in (findom F) \ (Seg n) by A15, XBOOLE_0:def_5; A19: Seg n c= findom F by A3, A16, FINSEQ_1:5; G . (Seg (n + 1)) = G . ((Seg n) \/ {(n + 1)}) by FINSEQ_1:9 .= g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . (n + 1))) by A6, A14, A19, A18 ; hence f . (n + 1) = G . (Seg (n + 1)) by A11, A12, A14, A17, A15, FUNCT_4:13, NAT_1:13; ::_thesis: verum end; end; end; hence f . (n + 1) = G . (Seg (n + 1)) ; ::_thesis: verum end; A20: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A10); hence g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A1, A9, A3, A4; ::_thesis: verum end; Lm2: for D being non empty set for F being FinSequence of D for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) proof let D be non empty set ; ::_thesis: for F being FinSequence of D for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let g be BinOp of D; ::_thesis: ( len F = 0 & g is having_a_unity & g is associative & g is commutative implies g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) ) assume that A1: len F = 0 and A2: g is having_a_unity and A3: ( g is associative & g is commutative ) ; ::_thesis: g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) F = {} by A1; then A4: dom F = {}. NAT ; thus g "**" F = the_unity_wrt g by A1, A2, Def1 .= g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A2, A3, A4, SETWISEO:31 ; ::_thesis: verum end; theorem :: FINSOP_1:3 for D being non empty set for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) proof let D be non empty set ; ::_thesis: for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let F be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) ) ( len F = 0 or len F >= 1 ) by NAT_1:14; hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g \$\$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) ) by Lm1, Lm2; ::_thesis: verum end; Lm3: for D being non empty set for g being BinOp of D st g is having_a_unity holds g "**" (<*> D) = the_unity_wrt g proof let D be non empty set ; ::_thesis: for g being BinOp of D st g is having_a_unity holds g "**" (<*> D) = the_unity_wrt g let g be BinOp of D; ::_thesis: ( g is having_a_unity implies g "**" (<*> D) = the_unity_wrt g ) A1: len (<*> D) = 0 ; assume g is having_a_unity ; ::_thesis: g "**" (<*> D) = the_unity_wrt g hence g "**" (<*> D) = the_unity_wrt g by A1, Def1; ::_thesis: verum end; Lm4: for D being non empty set for d being Element of D for g being BinOp of D holds g "**" <*d*> = d proof let D be non empty set ; ::_thesis: for d being Element of D for g being BinOp of D holds g "**" <*d*> = d let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d*> = d let g be BinOp of D; ::_thesis: g "**" <*d*> = d A1: len <*d*> = 1 by FINSEQ_1:39; then ex f being Function of NAT,D st ( f . 1 = <*d*> . 1 & ( for n being Element of NAT st 0 <> n & n < len <*d*> holds f . (n + 1) = g . ((f . n),(<*d*> . (n + 1))) ) & g "**" <*d*> = f . (len <*d*>) ) by Def1; hence g "**" <*d*> = d by A1, FINSEQ_1:def_8; ::_thesis: verum end; Lm5: for D being non empty set for d being Element of D for F being FinSequence of D for g being BinOp of D st len F >= 1 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) proof let D be non empty set ; ::_thesis: for d being Element of D for F being FinSequence of D for g being BinOp of D st len F >= 1 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let d be Element of D; ::_thesis: for F being FinSequence of D for g being BinOp of D st len F >= 1 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F >= 1 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let g be BinOp of D; ::_thesis: ( len F >= 1 implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) set G = F ^ <*d*>; A1: (F ^ <*d*>) . ((len F) + 1) = d by FINSEQ_1:42; A2: len (F ^ <*d*>) = (len F) + (len <*d*>) by FINSEQ_1:22 .= (len F) + 1 by FINSEQ_1:39 ; then 1 <= len (F ^ <*d*>) by NAT_1:12; then consider f1 being Function of NAT,D such that A3: f1 . 1 = (F ^ <*d*>) . 1 and A4: for n being Element of NAT st 0 <> n & n < len (F ^ <*d*>) holds f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) and A5: g "**" (F ^ <*d*>) = f1 . (len (F ^ <*d*>)) by Def1; assume A6: len F >= 1 ; ::_thesis: g "**" (F ^ <*d*>) = g . ((g "**" F),d) then consider f being Function of NAT,D such that A7: f . 1 = F . 1 and A8: for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = g . ((f . n),(F . (n + 1))) and A9: g "**" F = f . (len F) by Def1; defpred S1[ Element of NAT ] means ( 0 <> \$1 & \$1 < len (F ^ <*d*>) implies f . \$1 = f1 . \$1 ); A10: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A11: S1[n] ; ::_thesis: S1[n + 1] assume that A12: 0 <> n + 1 and A13: n + 1 < len (F ^ <*d*>) ; ::_thesis: f . (n + 1) = f1 . (n + 1) A14: n + 1 >= 1 by A12, NAT_1:14; now__::_thesis:_f_._(n_+_1)_=_f1_._(n_+_1) percases ( n + 1 = 1 or n + 1 > 1 ) by A14, XXREAL_0:1; supposeA15: n + 1 = 1 ; ::_thesis: f . (n + 1) = f1 . (n + 1) 1 in dom F by A6, FINSEQ_3:25; hence f . (n + 1) = f1 . (n + 1) by A7, A3, A15, FINSEQ_1:def_7; ::_thesis: verum end; supposeA16: n + 1 > 1 ; ::_thesis: f . (n + 1) = f1 . (n + 1) then n <> 0 ; then A17: f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) by A4, A13, NAT_1:12; A18: n + 1 <= len F by A2, A13, NAT_1:13; then A19: n < len F by NAT_1:13; 1 <= n + 1 by NAT_1:12; then A20: n + 1 in dom F by A18, FINSEQ_3:25; n + 1 > 0 + 1 by A16; then f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A19; hence f . (n + 1) = f1 . (n + 1) by A11, A13, A16, A17, A20, FINSEQ_1:def_7, NAT_1:12; ::_thesis: verum end; end; end; hence f . (n + 1) = f1 . (n + 1) ; ::_thesis: verum end; A21: S1[ 0 ] ; A22: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A10); g "**" (F ^ <*d*>) = g . ((f1 . (len F)),((F ^ <*d*>) . ((len F) + 1))) by A6, A2, A4, A5, XREAL_1:29; hence g "**" (F ^ <*d*>) = g . ((g "**" F),d) by A6, A9, A2, A1, A22, XREAL_1:29; ::_thesis: verum end; Lm6: for D being non empty set for d being Element of D for F being FinSequence of D for g being BinOp of D st g is having_a_unity & len F = 0 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) proof let D be non empty set ; ::_thesis: for d being Element of D for F being FinSequence of D for g being BinOp of D st g is having_a_unity & len F = 0 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let d be Element of D; ::_thesis: for F being FinSequence of D for g being BinOp of D st g is having_a_unity & len F = 0 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is having_a_unity & len F = 0 holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let g be BinOp of D; ::_thesis: ( g is having_a_unity & len F = 0 implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) assume that A1: g is having_a_unity and A2: len F = 0 ; ::_thesis: g "**" (F ^ <*d*>) = g . ((g "**" F),d) F = <*> D by A2; hence g "**" (F ^ <*d*>) = g "**" <*d*> by FINSEQ_1:34 .= d by Lm4 .= g . ((the_unity_wrt g),d) by A1, SETWISEO:15 .= g . ((g "**" F),d) by A1, A2, Def1 ; ::_thesis: verum end; theorem Th4: :: FINSOP_1:4 for D being non empty set for d being Element of D for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) proof let D be non empty set ; ::_thesis: for d being Element of D for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let d be Element of D; ::_thesis: for F being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let F be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds g "**" (F ^ <*d*>) = g . ((g "**" F),d) let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) ( len F >= 1 or len F = 0 ) by NAT_1:14; hence ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) by Lm5, Lm6; ::_thesis: verum end; theorem Th5: :: FINSOP_1:5 for D being non empty set for F, G being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) ) defpred S1[ FinSequence of D] means for F being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len \$1 >= 1 ) ) holds g "**" (F ^ \$1) = g . ((g "**" F),(g "**" \$1)); A1: for G being FinSequence of D for d being Element of D st S1[G] holds S1[G ^ <*d*>] proof let G be FinSequence of D; ::_thesis: for d being Element of D st S1[G] holds S1[G ^ <*d*>] let d be Element of D; ::_thesis: ( S1[G] implies S1[G ^ <*d*>] ) assume A2: S1[G] ; ::_thesis: S1[G ^ <*d*>] let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) holds g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) implies g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) ) assume that A3: g is associative and A4: ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) A5: now__::_thesis:_(_not_g_is_having_a_unity_implies_len_(F_^_G)_>=_1_) A6: len (F ^ G) = (len F) + (len G) by FINSEQ_1:22; assume not g is having_a_unity ; ::_thesis: len (F ^ G) >= 1 hence len (F ^ G) >= 1 by A4, A6, NAT_1:12; ::_thesis: verum end; A7: g "**" (F ^ (G ^ <*d*>)) = g "**" ((F ^ G) ^ <*d*>) by FINSEQ_1:32 .= g . ((g "**" (F ^ G)),d) by A5, Th4 ; now__::_thesis:_g_"**"_(F_^_(G_^_<*d*>))_=_g_._((g_"**"_F),(g_"**"_(G_^_<*d*>))) percases ( len G <> 0 or len G = 0 ) ; supposeA8: len G <> 0 ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) then len G >= 1 by NAT_1:14; hence g "**" (F ^ (G ^ <*d*>)) = g . ((g . ((g "**" F),(g "**" G))),d) by A2, A3, A4, A7 .= g . ((g "**" F),(g . ((g "**" G),d))) by A3, BINOP_1:def_3 .= g . ((g "**" F),(g "**" (G ^ <*d*>))) by A8, Th4, NAT_1:14 ; ::_thesis: verum end; suppose len G = 0 ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) then A9: G = {} ; hence g "**" (F ^ (G ^ <*d*>)) = g "**" (F ^ <*d*>) by FINSEQ_1:34 .= g . ((g "**" F),d) by A4, Th4 .= g . ((g "**" F),(g "**" <*d*>)) by Lm4 .= g . ((g "**" F),(g "**" (G ^ <*d*>))) by A9, FINSEQ_1:34 ; ::_thesis: verum end; end; end; hence g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) ; ::_thesis: verum end; A10: S1[ <*> D] proof let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) holds g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D))) let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) implies g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D))) ) assume that g is associative and A11: ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) ; ::_thesis: g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D))) thus g "**" (F ^ (<*> D)) = g "**" F by FINSEQ_1:34 .= g . ((g "**" F),(the_unity_wrt g)) by A11, SETWISEO:15 .= g . ((g "**" F),(g "**" (<*> D))) by A11, Lm3 ; ::_thesis: verum end; for G being FinSequence of D holds S1[G] from FINSEQ_2:sch_2(A10, A1); hence ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) ) ; ::_thesis: verum end; theorem Th6: :: FINSOP_1:6 for D being non empty set for d being Element of D for F being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds g "**" (<*d*> ^ F) = g . (d,(g "**" F)) proof let D be non empty set ; ::_thesis: for d being Element of D for F being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds g "**" (<*d*> ^ F) = g . (d,(g "**" F)) let d be Element of D; ::_thesis: for F being FinSequence of D for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds g "**" (<*d*> ^ F) = g . (d,(g "**" F)) let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds g "**" (<*d*> ^ F) = g . (d,(g "**" F)) let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or len F >= 1 ) implies g "**" (<*d*> ^ F) = g . (d,(g "**" F)) ) A1: len <*d*> = 1 by FINSEQ_1:39; assume ( g is associative & ( g is having_a_unity or len F >= 1 ) ) ; ::_thesis: g "**" (<*d*> ^ F) = g . (d,(g "**" F)) hence g "**" (<*d*> ^ F) = g . ((g "**" <*d*>),(g "**" F)) by A1, Th5 .= g . (d,(g "**" F)) by Lm4 ; ::_thesis: verum end; Lm7: for D being non empty set for F, G being FinSequence of D for g being BinOp of D st g is associative & g is commutative holds for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D st g is associative & g is commutative holds for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative holds for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: ( g is associative & g is commutative implies for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds g "**" F = g "**" G ) assume that A1: g is associative and A2: g is commutative ; ::_thesis: for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds g "**" F = g "**" G defpred S1[ Element of NAT ] means for H1, H2 being FinSequence of D st len H1 >= 1 & len H1 = \$1 & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds g "**" H1 = g "**" H2; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let H1, H2 be FinSequence of D; ::_thesis: ( len H1 >= 1 & len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds g "**" H1 = g "**" H2 ) assume that len H1 >= 1 and A5: len H1 = k + 1 and A6: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds g "**" H1 = g "**" H2 reconsider p = H2 | (Seg k) as FinSequence of D by FINSEQ_1:18; let f be Permutation of (dom H1); ::_thesis: ( ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) implies g "**" H1 = g "**" H2 ) A7: dom H1 = Seg (k + 1) by A5, FINSEQ_1:def_3; then A8: rng f = Seg (k + 1) by FUNCT_2:def_3; A9: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_ f_._n_is_Element_of_NAT let n be Element of NAT ; ::_thesis: ( n in dom f implies f . n is Element of NAT ) assume n in dom f ; ::_thesis: f . n is Element of NAT then f . n in Seg (k + 1) by A8, FUNCT_1:def_3; hence f . n is Element of NAT ; ::_thesis: verum end; A10: rng H2 c= D by FINSEQ_1:def_4; ( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ; then A11: dom f = Seg (k + 1) by A7, FUNCT_2:def_1; A12: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A13: f . (k + 1) in Seg (k + 1) by A11, A8, FUNCT_1:def_3; then reconsider n = f . (k + 1) as Element of NAT ; A14: dom H2 = Seg (k + 1) by A5, A6, FINSEQ_1:def_3; then H2 . (k + 1) in rng H2 by A12, FUNCT_1:def_3; then reconsider d = H2 . (k + 1) as Element of D by A10; A15: n <= k + 1 by A13, FINSEQ_1:1; then consider m2 being Nat such that A16: n + m2 = k + 1 by NAT_1:10; defpred S2[ Nat, set ] means \$2 = H1 . (n + \$1); 1 <= n by A13, FINSEQ_1:1; then consider m1 being Nat such that A17: 1 + m1 = n by NAT_1:10; reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def_12; A18: for j being Nat st j in Seg m2 holds ex x being set st S2[j,x] ; consider q2 being FinSequence such that A19: dom q2 = Seg m2 and A20: for k being Nat st k in Seg m2 holds S2[k,q2 . k] from FINSEQ_1:sch_1(A18); rng q2 c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q2 or x in D ) assume x in rng q2 ; ::_thesis: x in D then consider y being set such that A21: y in findom q2 and A22: x = q2 . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A21, SETWISEO:9; 1 <= y by A19, A21, FINSEQ_1:1; then A23: 1 <= n + y by NAT_1:12; y <= m2 by A19, A21, FINSEQ_1:1; then n + y <= len H1 by A5, A16, XREAL_1:7; then n + y in Seg (len H1) by A23, FINSEQ_1:1; then n + y in dom H1 by FINSEQ_1:def_3; then A24: H1 . (n + y) in rng H1 by FUNCT_1:def_3; rng H1 c= D by FINSEQ_1:def_4; then reconsider xx = H1 . (n + y) as Element of D by A24; xx in D ; hence x in D by A19, A20, A21, A22; ::_thesis: verum end; then reconsider q2 = q2 as FinSequence of D by FINSEQ_1:def_4; reconsider q1 = H1 | (Seg m1) as FinSequence of D by FINSEQ_1:18; defpred S3[ Nat, set ] means ( ( f . \$1 in dom q1 implies \$2 = f . \$1 ) & ( not f . \$1 in dom q1 implies for l being Element of NAT st l = f . \$1 holds \$2 = l - 1 ) ); A25: k <= k + 1 by NAT_1:12; then A26: Seg k c= Seg (k + 1) by FINSEQ_1:5; A27: for i being Nat st i in Seg k holds ex y being set st S3[i,y] proof let i be Nat; ::_thesis: ( i in Seg k implies ex y being set st S3[i,y] ) assume A28: i in Seg k ; ::_thesis: ex y being set st S3[i,y] now__::_thesis:_(_not_f_._i_in_dom_q1_implies_ex_y_being_set_st_ (_(_f_._i_in_dom_q1_implies_y_=_f_._i_)_&_(_not_f_._i_in_dom_q1_implies_for_t_being_Element_of_NAT_st_t_=_f_._i_holds_ y_=_t_-_1_)_)_) f . i in Seg (k + 1) by A11, A8, A26, A28, FUNCT_1:def_3; then reconsider j = f . i as Element of NAT ; assume A29: not f . i in dom q1 ; ::_thesis: ex y being set st ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) ) take y = j - 1; ::_thesis: ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) ) thus ( f . i in dom q1 implies y = f . i ) by A29; ::_thesis: ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) assume not f . i in dom q1 ; ::_thesis: for t being Element of NAT st t = f . i holds y = t - 1 let t be Element of NAT ; ::_thesis: ( t = f . i implies y = t - 1 ) assume t = f . i ; ::_thesis: y = t - 1 hence y = t - 1 ; ::_thesis: verum end; hence ex y being set st S3[i,y] ; ::_thesis: verum end; consider gg being FinSequence such that A30: dom gg = Seg k and A31: for i being Nat st i in Seg k holds S3[i,gg . i] from FINSEQ_1:sch_1(A27); A32: dom p = Seg k by A5, A6, A25, FINSEQ_1:17; m1 <= n by A17, NAT_1:11; then A33: m1 <= k + 1 by A15, XXREAL_0:2; then A34: dom q1 = Seg m1 by A5, FINSEQ_1:17; A35: now__::_thesis:_for_i,_l_being_Element_of_NAT_st_l_=_f_._i_&_not_f_._i_in_dom_q1_&_i_in_dom_gg_holds_ m1_+_2_<=_l let i, l be Element of NAT ; ::_thesis: ( l = f . i & not f . i in dom q1 & i in dom gg implies m1 + 2 <= l ) assume that A36: l = f . i and A37: not f . i in dom q1 and A38: i in dom gg ; ::_thesis: m1 + 2 <= l A39: ( l < 1 or m1 < l ) by A34, A36, A37, FINSEQ_1:1; A40: now__::_thesis:_not_m1_+_1_=_l assume m1 + 1 = l ; ::_thesis: contradiction then k + 1 = i by A12, A11, A17, A26, A30, A36, A38, FUNCT_1:def_4; then k + 1 <= k + 0 by A30, A38, FINSEQ_1:1; hence contradiction by XREAL_1:6; ::_thesis: verum end; f . i in rng f by A11, A26, A30, A38, FUNCT_1:def_3; then m1 + 1 <= l by A8, A36, A39, FINSEQ_1:1, NAT_1:13; then m1 + 1 < l by A40, XXREAL_0:1; then (m1 + 1) + 1 <= l by NAT_1:13; hence m1 + 2 <= l ; ::_thesis: verum end; 1 + k = 1 + (m1 + m2) by A17, A16; then A41: m1 <= k by NAT_1:11; A42: rng gg c= dom p proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng gg or y in dom p ) assume y in rng gg ; ::_thesis: y in dom p then consider x being set such that A43: x in findom gg and A44: gg . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A43, SETWISEO:9; now__::_thesis:_y_in_dom_p percases ( f . x in dom q1 or not f . x in dom q1 ) ; supposeA45: f . x in dom q1 ; ::_thesis: y in dom p A46: dom q1 c= dom p by A41, A34, A32, FINSEQ_1:5; f . x = gg . x by A30, A31, A43, A45; hence y in dom p by A44, A45, A46; ::_thesis: verum end; supposeA47: not f . x in dom q1 ; ::_thesis: y in dom p reconsider j = f . x as Element of NAT by A11, A26, A9, A30, A43; A48: f . x in Seg (k + 1) by A11, A8, A26, A30, A43, FUNCT_1:def_3; ( j < 1 or m1 < j ) by A34, A47, FINSEQ_1:1; then reconsider l = j - 1 as Element of NAT by A48, FINSEQ_1:1, NAT_1:20; j <= k + 1 by A48, FINSEQ_1:1; then A49: l <= (k + 1) - 1 by XREAL_1:9; m1 + 2 <= j by A35, A43, A47; then A50: (m1 + 2) - 1 <= l by XREAL_1:9; 1 <= m1 + 1 by NAT_1:12; then A51: 1 <= l by A50, XXREAL_0:2; gg . x = j - 1 by A30, A31, A43, A47; hence y in dom p by A32, A44, A51, A49, FINSEQ_1:1; ::_thesis: verum end; end; end; hence y in dom p ; ::_thesis: verum end; A52: len q1 = m1 by A5, A33, FINSEQ_1:17; A53: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_ H1_._((len_(q1_^_<*d*>))_+_j)_=_q2_._j let j be Nat; ::_thesis: ( j in dom q2 implies H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j ) assume A54: j in dom q2 ; ::_thesis: H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22 .= n by A17, FINSEQ_1:39 ; hence H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j by A19, A20, A54; ::_thesis: verum end; set q = q1 ^ q2; A55: len q2 = m2 by A19, FINSEQ_1:def_3; then A56: len (q1 ^ q2) = m1 + m2 by A52, FINSEQ_1:22; then A57: dom (q1 ^ q2) = Seg k by A17, A16, FINSEQ_1:def_3; then reconsider gg = gg as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A32, A30, A42, FUNCT_2:2; A58: len p = k by A5, A6, A25, FINSEQ_1:17; A59: rng gg = dom (q1 ^ q2) proof thus rng gg c= dom (q1 ^ q2) by A17, A16, A56, A32, A42, FINSEQ_1:def_3; :: according to XBOOLE_0:def_10 ::_thesis: dom (q1 ^ q2) c= rng gg let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (q1 ^ q2) or y in rng gg ) assume A60: y in dom (q1 ^ q2) ; ::_thesis: y in rng gg then reconsider j = y as Element of NAT ; consider x being set such that A61: x in dom f and A62: f . x = y by A8, A26, A57, A60, FUNCT_1:def_3; reconsider x = x as Element of NAT by A11, A61; now__::_thesis:_y_in_rng_gg percases ( x in dom gg or not x in dom gg ) ; supposeA63: x in dom gg ; ::_thesis: y in rng gg now__::_thesis:_y_in_rng_gg percases ( f . x in dom q1 or not f . x in dom q1 ) ; suppose f . x in dom q1 ; ::_thesis: y in rng gg then gg . x = f . x by A30, A31, A63; hence y in rng gg by A62, A63, FUNCT_1:def_3; ::_thesis: verum end; supposeA64: not f . x in dom q1 ; ::_thesis: y in rng gg j <= k by A57, A60, FINSEQ_1:1; then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7; then j + 1 in rng f by A8, FINSEQ_1:1; then consider x1 being set such that A65: x1 in dom f and A66: f . x1 = j + 1 by FUNCT_1:def_3; A67: now__::_thesis:_x1_in_dom_gg assume not x1 in dom gg ; ::_thesis: contradiction then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A65, XBOOLE_0:def_5; then x1 in {(k + 1)} by FINSEQ_3:15; then A68: j + 1 = m1 + 1 by A17, A66, TARSKI:def_1; 1 <= j by A57, A60, FINSEQ_1:1; hence contradiction by A34, A62, A64, A68, FINSEQ_1:1; ::_thesis: verum end; ( j < 1 or m1 < j ) by A34, A62, A64, FINSEQ_1:1; then not j + 1 <= m1 by A57, A60, FINSEQ_1:1, NAT_1:13; then not f . x1 in dom q1 by A34, A66, FINSEQ_1:1; then gg . x1 = (j + 1) - 1 by A30, A31, A66, A67 .= y ; hence y in rng gg by A67, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence y in rng gg ; ::_thesis: verum end; supposeA69: not x in dom gg ; ::_thesis: y in rng gg j <= k by A57, A60, FINSEQ_1:1; then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7; then j + 1 in rng f by A8, FINSEQ_1:1; then consider x1 being set such that A70: x1 in dom f and A71: f . x1 = j + 1 by FUNCT_1:def_3; x in (Seg (k + 1)) \ (Seg k) by A7, A30, A61, A69, XBOOLE_0:def_5; then x in {(k + 1)} by FINSEQ_3:15; then A72: x = k + 1 by TARSKI:def_1; A73: now__::_thesis:_x1_in_dom_gg assume not x1 in dom gg ; ::_thesis: contradiction then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A70, XBOOLE_0:def_5; then x1 in {(k + 1)} by FINSEQ_3:15; then j + 1 = j + 0 by A62, A72, A71, TARSKI:def_1; hence contradiction ; ::_thesis: verum end; m1 <= j by A17, A62, A72, XREAL_1:29; then not j + 1 <= m1 by NAT_1:13; then not f . x1 in dom q1 by A34, A71, FINSEQ_1:1; then gg . x1 = (j + 1) - 1 by A30, A31, A71, A73 .= y ; hence y in rng gg by A73, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence y in rng gg ; ::_thesis: verum end; assume A74: for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ; ::_thesis: g "**" H1 = g "**" H2 then A75: H2 . (k + 1) = H1 . (f . (k + 1)) by A14, FINSEQ_1:4; A76: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*d*>)_holds_ H1_._j_=_(q1_^_<*d*>)_._j let j be Nat; ::_thesis: ( j in dom (q1 ^ <*d*>) implies H1 . j = (q1 ^ <*d*>) . j ) assume A77: j in dom (q1 ^ <*d*>) ; ::_thesis: H1 . j = (q1 ^ <*d*>) . j A78: now__::_thesis:_(_j_in_Seg_m1_implies_H1_._j_=_(q1_^_<*d*>)_._j_) assume j in Seg m1 ; ::_thesis: H1 . j = (q1 ^ <*d*>) . j then A79: j in dom q1 by A5, A33, FINSEQ_1:17; then q1 . j = H1 . j by FUNCT_1:47; hence H1 . j = (q1 ^ <*d*>) . j by A79, FINSEQ_1:def_7; ::_thesis: verum end; A80: now__::_thesis:_(_j_in_{n}_implies_(q1_^_<*d*>)_._j_=_H1_._j_) ( 1 in Seg 1 & len <*d*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39; then 1 in dom <*d*> by FINSEQ_1:def_3; then A81: (q1 ^ <*d*>) . ((len q1) + 1) = <*d*> . 1 by FINSEQ_1:def_7; assume j in {n} ; ::_thesis: (q1 ^ <*d*>) . j = H1 . j then j = n by TARSKI:def_1; hence (q1 ^ <*d*>) . j = H1 . j by A75, A17, A52, A81, FINSEQ_1:40; ::_thesis: verum end; len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22 .= m1 + 1 by FINSEQ_1:40 ; then j in Seg (m1 + 1) by A77, FINSEQ_1:def_3; then j in (Seg m1) \/ {n} by A17, FINSEQ_1:9; hence H1 . j = (q1 ^ <*d*>) . j by A78, A80, XBOOLE_0:def_3; ::_thesis: verum end; gg is one-to-one proof let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y1 in findom gg or not b1 in findom gg or not gg . y1 = gg . b1 or y1 = b1 ) let y2 be set ; ::_thesis: ( not y1 in findom gg or not y2 in findom gg or not gg . y1 = gg . y2 or y1 = y2 ) assume that A82: y1 in dom gg and A83: y2 in dom gg and A84: gg . y1 = gg . y2 ; ::_thesis: y1 = y2 reconsider j1 = y1, j2 = y2 as Element of NAT by A30, A82, A83; A85: f . y2 in Seg (k + 1) by A11, A8, A26, A30, A83, FUNCT_1:def_3; A86: f . y1 in Seg (k + 1) by A11, A8, A26, A30, A82, FUNCT_1:def_3; then reconsider a = f . y1, b = f . y2 as Element of NAT by A85; now__::_thesis:_y1_=_y2 percases ( ( f . y1 in dom q1 & f . y2 in dom q1 ) or ( f . y1 in dom q1 & not f . y2 in dom q1 ) or ( not f . y1 in dom q1 & f . y2 in dom q1 ) or ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ) ; suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then ( gg . j1 = f . y1 & gg . j2 = f . y2 ) by A30, A31, A82, A83; hence y1 = y2 by A11, A26, A30, A82, A83, A84, FUNCT_1:def_4; ::_thesis: verum end; supposeA87: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then A88: a <= m1 by A34, FINSEQ_1:1; ( gg . j1 = a & gg . j2 = b - 1 ) by A30, A31, A82, A83, A87; then A89: (b - 1) + 1 <= m1 + 1 by A84, A88, XREAL_1:6; 1 <= b by A85, FINSEQ_1:1; then A90: b in Seg (m1 + 1) by A89, FINSEQ_1:1; not b in Seg m1 by A5, A33, A87, FINSEQ_1:17; then b in (Seg (m1 + 1)) \ (Seg m1) by A90, XBOOLE_0:def_5; then b in {(m1 + 1)} by FINSEQ_3:15; then b = m1 + 1 by TARSKI:def_1; then y2 = k + 1 by A12, A11, A17, A26, A30, A83, FUNCT_1:def_4; hence y1 = y2 by A30, A83, FINSEQ_3:8; ::_thesis: verum end; supposeA91: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then A92: b <= m1 by A34, FINSEQ_1:1; ( gg . j1 = a - 1 & gg . j2 = b ) by A30, A31, A82, A83, A91; then A93: (a - 1) + 1 <= m1 + 1 by A84, A92, XREAL_1:6; 1 <= a by A86, FINSEQ_1:1; then A94: a in Seg (m1 + 1) by A93, FINSEQ_1:1; not a in Seg m1 by A5, A33, A91, FINSEQ_1:17; then a in (Seg (m1 + 1)) \ (Seg m1) by A94, XBOOLE_0:def_5; then a in {(m1 + 1)} by FINSEQ_3:15; then a = m1 + 1 by TARSKI:def_1; then y1 = k + 1 by A12, A11, A17, A26, A30, A82, FUNCT_1:def_4; hence y1 = y2 by A30, A82, FINSEQ_3:8; ::_thesis: verum end; supposeA95: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then gg . j2 = b - 1 by A30, A31, A83; then A96: gg . y2 = b + (- 1) ; gg . j1 = a - 1 by A30, A31, A82, A95; then gg . j1 = a + (- 1) ; then a = b by A84, A96, XCMPLX_1:2; hence y1 = y2 by A11, A26, A30, A82, A83, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence y1 = y2 ; ::_thesis: verum end; then reconsider gg = gg as Permutation of (dom (q1 ^ q2)) by A59, FUNCT_2:57; (len (q1 ^ <*d*>)) + (len q2) = ((len q1) + (len <*d*>)) + m2 by A55, FINSEQ_1:22 .= k + 1 by A17, A16, A52, FINSEQ_1:40 ; then dom H1 = Seg ((len (q1 ^ <*d*>)) + (len q2)) by A5, FINSEQ_1:def_3; then A97: H1 = (q1 ^ <*d*>) ^ q2 by A76, A53, FINSEQ_1:def_7; A98: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_ p_._i_=_(q1_^_q2)_._(gg_._i) let i be Element of NAT ; ::_thesis: ( i in dom p implies p . i = (q1 ^ q2) . (gg . i) ) assume A99: i in dom p ; ::_thesis: p . i = (q1 ^ q2) . (gg . i) then f . i in rng f by A11, A26, A32, FUNCT_1:def_3; then reconsider j = f . i as Element of NAT by A8; now__::_thesis:_p_._i_=_(q1_^_q2)_._(gg_._i) percases ( f . i in dom q1 or not f . i in dom q1 ) ; supposeA100: f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (gg . i) then A101: ( f . i = gg . i & H1 . j = q1 . j ) by A32, A31, A99, FUNCT_1:47; ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47; hence p . i = (q1 ^ q2) . (gg . i) by A100, A101, FINSEQ_1:def_7; ::_thesis: verum end; supposeA102: not f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (gg . i) then m1 + 2 <= j by A32, A30, A35, A99; then A103: (m1 + 2) - 1 <= j - 1 by XREAL_1:9; m1 < m1 + 1 by XREAL_1:29; then A104: m1 < j - 1 by A103, XXREAL_0:2; then m1 < j by XREAL_1:146, XXREAL_0:2; then reconsider j1 = j - 1 as Element of NAT by NAT_1:20; A105: not j1 in dom q1 by A34, A104, FINSEQ_1:1; A106: gg . i = j - 1 by A32, A31, A99, A102; then j - 1 in dom (q1 ^ q2) by A32, A30, A59, A99, FUNCT_1:def_3; then consider a being Nat such that A107: a in dom q2 and A108: j1 = (len q1) + a by A105, FINSEQ_1:25; A109: len <*d*> = 1 by FINSEQ_1:39; A110: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47; A111: H1 = q1 ^ (<*d*> ^ q2) by A97, FINSEQ_1:32; j in dom H1 by A7, A11, A8, A26, A32, A99, FUNCT_1:def_3; then consider b being Nat such that A112: b in dom (<*d*> ^ q2) and A113: j = (len q1) + b by A102, A111, FINSEQ_1:25; A114: H1 . j = (<*d*> ^ q2) . b by A111, A112, A113, FINSEQ_1:def_7; A115: b = 1 + a by A108, A113; (q1 ^ q2) . (j - 1) = q2 . a by A107, A108, FINSEQ_1:def_7; hence p . i = (q1 ^ q2) . (gg . i) by A106, A110, A107, A114, A115, A109, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence p . i = (q1 ^ q2) . (gg . i) ; ::_thesis: verum end; now__::_thesis:_g_"**"_H1_=_g_"**"_H2 percases ( len p <> 0 or len p = 0 ) ; supposeA116: len p <> 0 ; ::_thesis: g "**" H1 = g "**" H2 A117: H2 = p ^ <*d*> by A5, A6, FINSEQ_3:55; g "**" p = g "**" (q1 ^ q2) by A4, A17, A16, A58, A56, A98, A116, NAT_1:14; then A118: g "**" H2 = g . ((g "**" (q1 ^ q2)),d) by A116, A117, Th4, NAT_1:14; now__::_thesis:_g_"**"_H1_=_g_"**"_H2 percases ( ( len q1 <> 0 & len q2 <> 0 ) or ( len q1 = 0 & len q2 <> 0 ) or ( len q1 <> 0 & len q2 = 0 ) or ( len q1 = 0 & len q2 = 0 ) ) ; supposeA119: ( len q1 <> 0 & len q2 <> 0 ) ; ::_thesis: g "**" H1 = g "**" H2 ( len (<*d*> ^ q2) = (len <*d*>) + (len q2) & len <*d*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; then A120: len (<*d*> ^ q2) >= 1 by NAT_1:12; A121: len q1 >= 1 by A119, NAT_1:14; len q2 >= 1 by A119, NAT_1:14; then g "**" H2 = g . ((g . ((g "**" q1),(g "**" q2))),d) by A1, A118, A121, Th5 .= g . ((g "**" q1),(g . ((g "**" q2),d))) by A1, BINOP_1:def_3 .= g . ((g "**" q1),(g . (d,(g "**" q2)))) by A2, BINOP_1:def_2 .= g . ((g "**" q1),(g "**" (<*d*> ^ q2))) by A1, A119, Th6, NAT_1:14 .= g "**" (q1 ^ (<*d*> ^ q2)) by A1, A121, A120, Th5 .= g "**" H1 by A97, FINSEQ_1:32 ; hence g "**" H1 = g "**" H2 ; ::_thesis: verum end; suppose ( len q1 = 0 & len q2 <> 0 ) ; ::_thesis: g "**" H1 = g "**" H2 then A122: q1 = {} ; then A123: H1 = <*d*> ^ q2 by A97, FINSEQ_1:34 .= <*d*> ^ (q1 ^ q2) by A122, FINSEQ_1:34 ; g "**" H2 = g . (d,(g "**" (q1 ^ q2))) by A2, A118, BINOP_1:def_2 .= g "**" (<*d*> ^ (q1 ^ q2)) by A1, A17, A16, A58, A56, A116, Th6, NAT_1:14 ; hence g "**" H1 = g "**" H2 by A123; ::_thesis: verum end; suppose ( len q1 <> 0 & len q2 = 0 ) ; ::_thesis: g "**" H1 = g "**" H2 then A124: q2 = {} ; then H1 = q1 ^ <*d*> by A97, FINSEQ_1:34 .= (q1 ^ q2) ^ <*d*> by A124, FINSEQ_1:34 ; hence g "**" H1 = g "**" H2 by A17, A16, A58, A56, A116, A118, Th4, NAT_1:14; ::_thesis: verum end; suppose ( len q1 = 0 & len q2 = 0 ) ; ::_thesis: g "**" H1 = g "**" H2 then len (q1 ^ q2) = 0 + 0 by FINSEQ_1:22; hence g "**" H1 = g "**" H2 by A5, A6, A17, A16, A56, A116, FINSEQ_1:17; ::_thesis: verum end; end; end; hence g "**" H1 = g "**" H2 ; ::_thesis: verum end; supposeA125: len p = 0 ; ::_thesis: g "**" H1 = g "**" H2 then dom H1 = {1} by A5, A58, FINSEQ_1:2, FINSEQ_1:def_3; then A126: ( dom f = {1} & rng f = {1} ) by FUNCT_2:def_1, FUNCT_2:def_3; 1 in {1} by TARSKI:def_1; then f . 1 in {1} by A126, FUNCT_1:def_3; then H1 . 1 = H2 . 1 by A75, A58, A125, TARSKI:def_1; then H1 = <*d*> by A5, A58, A125, FINSEQ_1:40; hence g "**" H1 = g "**" H2 by A5, A6, A58, A125, FINSEQ_1:40; ::_thesis: verum end; end; end; hence g "**" H1 = g "**" H2 ; ::_thesis: verum end; end; let f be Permutation of (dom F); ::_thesis: ( len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) implies g "**" F = g "**" G ) A127: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A127, A3); hence ( len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) implies g "**" F = g "**" G ) ; ::_thesis: verum end; Lm8: for D being non empty set for F, G being FinSequence of D for g being BinOp of D for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds g "**" F = g "**" G let P be Permutation of (dom F); ::_thesis: ( g is having_a_unity & len F = 0 & G = F * P implies g "**" F = g "**" G ) assume that A1: g is having_a_unity and A2: len F = 0 ; ::_thesis: ( not G = F * P or g "**" F = g "**" G ) assume A3: G = F * P ; ::_thesis: g "**" F = g "**" G F = {} by A2; then G = {} by A3, RELAT_1:39; then A4: len G = 0 ; thus g "**" F = the_unity_wrt g by A1, A2, Def1 .= g "**" G by A1, A4, Def1 ; ::_thesis: verum end; theorem Th7: :: FINSOP_1:7 for D being non empty set for F, G being FinSequence of D for g being BinOp of D for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds g "**" F = g "**" G let P be Permutation of (dom F); ::_thesis: ( g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P implies g "**" F = g "**" G ) assume that A1: ( g is commutative & g is associative ) and A2: ( g is having_a_unity or len F >= 1 ) ; ::_thesis: ( not G = F * P or g "**" F = g "**" G ) assume A3: G = F * P ; ::_thesis: g "**" F = g "**" G now__::_thesis:_g_"**"_F_=_g_"**"_G percases ( len F = 0 or len F <> 0 ) ; suppose len F = 0 ; ::_thesis: g "**" F = g "**" G hence g "**" F = g "**" G by A2, A3, Lm8; ::_thesis: verum end; supposeA4: len F <> 0 ; ::_thesis: g "**" F = g "**" G ( len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (P . i) ) ) by A3, FINSEQ_2:44, FUNCT_1:12; hence g "**" F = g "**" G by A1, A4, Lm7, NAT_1:14; ::_thesis: verum end; end; end; hence g "**" F = g "**" G ; ::_thesis: verum end; Lm9: for D being non empty set for F, G being FinSequence of D for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 implies g "**" F = g "**" G ) assume that A1: ( g is associative & g is commutative ) and A2: F is one-to-one and A3: G is one-to-one and A4: rng F = rng G and A5: len F >= 1 ; ::_thesis: g "**" F = g "**" G A6: len F = len G by A2, A3, A4, FINSEQ_1:48; set P = (F ") * G; A7: dom (F ") = rng F by A2, FUNCT_1:33; then A8: dom ((F ") * G) = dom G by A4, RELAT_1:27 .= Seg (len F) by A6, FINSEQ_1:def_3 .= dom F by FINSEQ_1:def_3 ; rng (F ") = dom F by A2, FUNCT_1:33; then A9: rng ((F ") * G) c= dom F by RELAT_1:26; dom F = Seg (len F) by FINSEQ_1:def_3; then reconsider P = (F ") * G as Function of (dom F),(dom F) by A5, A8, A9, FUNCT_2:def_1, RELSET_1:4; rng P = rng (F ") by A4, A7, RELAT_1:28 .= dom F by A2, FUNCT_1:33 ; then reconsider P = P as Permutation of (dom F) by A2, A3, FUNCT_2:57; F * P = (F * (F ")) * G by RELAT_1:36 .= (id (rng G)) * G by A2, A4, FUNCT_1:39 .= G by RELAT_1:54 ; hence g "**" F = g "**" G by A1, A5, Th7; ::_thesis: verum end; Lm10: for D being non empty set for F, G being FinSequence of D for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: ( len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G ) assume that A1: ( len F = 0 & g is having_a_unity ) and A2: ( F is one-to-one & G is one-to-one & rng F = rng G ) ; ::_thesis: g "**" F = g "**" G ( len G = len F & g "**" F = the_unity_wrt g ) by A1, A2, Def1, FINSEQ_1:48; hence g "**" F = g "**" G by A1, Def1; ::_thesis: verum end; theorem :: FINSOP_1:8 for D being non empty set for F, G being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G proof let D be non empty set ; ::_thesis: for F, G being FinSequence of D for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds g "**" F = g "**" G let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G ) ( len F >= 1 or len F = 0 ) by NAT_1:14; hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G ) by Lm9, Lm10; ::_thesis: verum end; Lm11: for D being non empty set for F being FinSequence of D for g being BinOp of D st len F = 1 holds g "**" F = F . 1 proof let D be non empty set ; ::_thesis: for F being FinSequence of D for g being BinOp of D st len F = 1 holds g "**" F = F . 1 let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 1 holds g "**" F = F . 1 let g be BinOp of D; ::_thesis: ( len F = 1 implies g "**" F = F . 1 ) assume A1: len F = 1 ; ::_thesis: g "**" F = F . 1 then F = <*(F . 1)*> by FINSEQ_1:40 .= <*(F /. 1)*> by A1, FINSEQ_4:15 ; hence g "**" F = F /. 1 by Lm4 .= F . 1 by A1, FINSEQ_4:15 ; ::_thesis: verum end; Lm12: for D being non empty set for F, G, H being FinSequence of D for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) holds g "**" H = g . ((g "**" F),(g "**" G)) proof let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) holds g "**" H = g . ((g "**" F),(g "**" G)) let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) holds g "**" H = g . ((g "**" F),(g "**" G)) let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) implies g "**" H = g . ((g "**" F),(g "**" G)) ) assume that A1: g is associative and A2: g is commutative ; ::_thesis: ( not len F >= 1 or not len F = len G or not len F = len H or ex k being Element of NAT st ( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) ) defpred S1[ Element of NAT ] means for F, G, H being FinSequence of D st len F >= 1 & len F = \$1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) holds g "**" H = g . ((g "**" F),(g "**" G)); A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let F, G, H be FinSequence of D; ::_thesis: ( len F >= 1 & len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ) implies g "**" H = g . ((g "**" F),(g "**" G)) ) assume that len F >= 1 and A5: len F = k + 1 and A6: len F = len G and A7: len F = len H and A8: for k being Element of NAT st k in dom F holds H . k = g . ((F . k),(G . k)) ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G)) reconsider f = F | (Seg k), gg = G | (Seg k), h = H | (Seg k) as FinSequence of D by FINSEQ_1:18; A9: len h = k by A5, A7, FINSEQ_3:53; A10: len f = k by A5, FINSEQ_3:53; A11: len gg = k by A5, A6, FINSEQ_3:53; A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ h_._i_=_g_._((f_._i),(gg_._i)) k <= k + 1 by NAT_1:12; then Seg (len f) c= Seg (len F) by A5, A10, FINSEQ_1:5; then Seg (len f) c= dom F by FINSEQ_1:def_3; then A13: dom f c= dom F by FINSEQ_1:def_3; let i be Element of NAT ; ::_thesis: ( i in dom f implies h . i = g . ((f . i),(gg . i)) ) assume A14: i in dom f ; ::_thesis: h . i = g . ((f . i),(gg . i)) then i in Seg (len gg) by A10, A11, FINSEQ_1:def_3; then i in dom gg by FINSEQ_1:def_3; then A15: G . i = gg . i by FUNCT_1:47; i in Seg (len h) by A10, A9, A14, FINSEQ_1:def_3; then i in dom h by FINSEQ_1:def_3; then A16: H . i = h . i by FUNCT_1:47; F . i = f . i by A14, FUNCT_1:47; hence h . i = g . ((f . i),(gg . i)) by A8, A14, A15, A16, A13; ::_thesis: verum end; now__::_thesis:_g_"**"_H_=_g_._((g_"**"_F),(g_"**"_G)) percases ( len f >= 1 or len f = 0 ) by NAT_1:14; supposeA17: len f >= 1 ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G)) A18: rng H c= D by FINSEQ_1:def_4; A19: ( rng F c= D & rng G c= D ) by FINSEQ_1:def_4; A20: k + 1 in Seg (k + 1) by FINSEQ_1:4; then k + 1 in dom G by A5, A6, FINSEQ_1:def_3; then A21: G . (k + 1) in rng G by FUNCT_1:def_3; k + 1 in dom H by A5, A7, A20, FINSEQ_1:def_3; then A22: H . (k + 1) in rng H by FUNCT_1:def_3; A23: k + 1 in dom F by A5, A20, FINSEQ_1:def_3; then F . (k + 1) in rng F by FUNCT_1:def_3; then reconsider d = F . (k + 1), d1 = G . (k + 1), d2 = H . (k + 1) as Element of D by A21, A22, A19, A18; A24: d2 = g . ((F . (k + 1)),(G . (k + 1))) by A8, A23; F = f ^ <*d*> by A5, FINSEQ_3:55; then A25: g "**" F = g . ((g "**" f),d) by A17, Th4; G = gg ^ <*d1*> by A5, A6, FINSEQ_3:55; then A26: g "**" G = g . ((g "**" gg),d1) by A10, A11, A17, Th4; A27: H = h ^ <*d2*> by A5, A7, FINSEQ_3:55; g "**" h = g . ((g "**" f),(g "**" gg)) by A4, A10, A11, A9, A12, A17; hence g "**" H = g . ((g . ((g "**" f),(g "**" gg))),(g . (d,d1))) by A10, A9, A17, A27, A24, Th4 .= g . ((g . ((g . ((g "**" f),(g "**" gg))),d)),d1) by A1, BINOP_1:def_3 .= g . ((g . ((g "**" f),(g . ((g "**" gg),d)))),d1) by A1, BINOP_1:def_3 .= g . ((g . ((g "**" f),(g . (d,(g "**" gg))))),d1) by A2, BINOP_1:def_2 .= g . ((g . ((g "**" F),(g "**" gg))),d1) by A1, A25, BINOP_1:def_3 .= g . ((g "**" F),(g "**" G)) by A1, A26, BINOP_1:def_3 ; ::_thesis: verum end; supposeA28: len f = 0 ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G)) then A29: ( g "**" G = G . 1 & 1 in dom F ) by A5, A6, A10, Lm11, FINSEQ_3:25; ( g "**" H = H . 1 & g "**" F = F . 1 ) by A5, A7, A10, A28, Lm11; hence g "**" H = g . ((g "**" F),(g "**" G)) by A8, A29; ::_thesis: verum end; end; end; hence g "**" H = g . ((g "**" F),(g "**" G)) ; ::_thesis: verum end; end; assume A30: ( len F >= 1 & len F = len G & len F = len H ) ; ::_thesis: ( ex k being Element of NAT st ( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) ) A31: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A31, A3); hence ( ex k being Element of NAT st ( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) ) by A30; ::_thesis: verum end; Lm13: for D being non empty set for F, G, H being FinSequence of D for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds g "**" F = g . ((g "**" G),(g "**" H)) proof let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds g "**" F = g . ((g "**" G),(g "**" H)) let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds g "**" F = g . ((g "**" G),(g "**" H)) let g be BinOp of D; ::_thesis: ( g is having_a_unity & len F = 0 & len F = len G & len F = len H implies g "**" F = g . ((g "**" G),(g "**" H)) ) assume that A1: g is having_a_unity and A2: len F = 0 and A3: len F = len G and A4: len F = len H ; ::_thesis: g "**" F = g . ((g "**" G),(g "**" H)) thus g "**" F = the_unity_wrt g by A1, A2, Def1 .= g . ((the_unity_wrt g),(the_unity_wrt g)) by A1, SETWISEO:15 .= g . ((g "**" G),(the_unity_wrt g)) by A1, A2, A3, Def1 .= g . ((g "**" G),(g "**" H)) by A1, A2, A4, Def1 ; ::_thesis: verum end; theorem :: FINSOP_1:9 for D being non empty set for F, G, H being FinSequence of D for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds F . k = g . ((G . k),(H . k)) ) holds g "**" F = g . ((g "**" G),(g "**" H)) proof let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds F . k = g . ((G . k),(H . k)) ) holds g "**" F = g . ((g "**" G),(g "**" H)) let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds F . k = g . ((G . k),(H . k)) ) holds g "**" F = g . ((g "**" G),(g "**" H)) let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds F . k = g . ((G . k),(H . k)) ) implies g "**" F = g . ((g "**" G),(g "**" H)) ) A1: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def_3; A2: ( len F = 0 or len F >= 1 ) by NAT_1:14; assume ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) ) ; ::_thesis: ( not len F = len G or not len F = len H or ex k being Element of NAT st ( k in dom F & not F . k = g . ((G . k),(H . k)) ) or g "**" F = g . ((g "**" G),(g "**" H)) ) hence ( not len F = len G or not len F = len H or ex k being Element of NAT st ( k in dom F & not F . k = g . ((G . k),(H . k)) ) or g "**" F = g . ((g "**" G),(g "**" H)) ) by A1, A2, Lm12, Lm13; ::_thesis: verum end; theorem :: FINSOP_1:10 for D being non empty set for g being BinOp of D st g is having_a_unity holds g "**" (<*> D) = the_unity_wrt g by Lm3; theorem :: FINSOP_1:11 for D being non empty set for d being Element of D for g being BinOp of D holds g "**" <*d*> = d by Lm4; theorem Th12: :: FINSOP_1:12 for D being non empty set for d1, d2 being Element of D for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2) let d1, d2 be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2) let g be BinOp of D; ::_thesis: g "**" <*d1,d2*> = g . (d1,d2) A1: len <*d1*> = 1 by FINSEQ_1:39; thus g "**" <*d1,d2*> = g "**" (<*d1*> ^ <*d2*>) by FINSEQ_1:def_9 .= g . ((g "**" <*d1*>),d2) by A1, Th4 .= g . (d1,d2) by Lm4 ; ::_thesis: verum end; theorem :: FINSOP_1:13 for D being non empty set for d1, d2 being Element of D for g being BinOp of D st g is commutative holds g "**" <*d1,d2*> = g "**" <*d2,d1*> proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for g being BinOp of D st g is commutative holds g "**" <*d1,d2*> = g "**" <*d2,d1*> let d1, d2 be Element of D; ::_thesis: for g being BinOp of D st g is commutative holds g "**" <*d1,d2*> = g "**" <*d2,d1*> let g be BinOp of D; ::_thesis: ( g is commutative implies g "**" <*d1,d2*> = g "**" <*d2,d1*> ) assume A1: g is commutative ; ::_thesis: g "**" <*d1,d2*> = g "**" <*d2,d1*> thus g "**" <*d1,d2*> = g . (d1,d2) by Th12 .= g . (d2,d1) by A1, BINOP_1:def_2 .= g "**" <*d2,d1*> by Th12 ; ::_thesis: verum end; theorem Th14: :: FINSOP_1:14 for D being non empty set for d1, d2, d3 being Element of D for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) proof let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) let d1, d2, d3 be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) let g be BinOp of D; ::_thesis: g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) A1: len <*d1,d2*> = 2 by FINSEQ_1:44; thus g "**" <*d1,d2,d3*> = g "**" (<*d1,d2*> ^ <*d3*>) by FINSEQ_1:43 .= g . ((g "**" <*d1,d2*>),d3) by A1, Th4 .= g . ((g . (d1,d2)),d3) by Th12 ; ::_thesis: verum end; theorem :: FINSOP_1:15 for D being non empty set for d1, d2, d3 being Element of D for g being BinOp of D st g is commutative holds g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> proof let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D for g being BinOp of D st g is commutative holds g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> let d1, d2, d3 be Element of D; ::_thesis: for g being BinOp of D st g is commutative holds g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> let g be BinOp of D; ::_thesis: ( g is commutative implies g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> ) assume A1: g is commutative ; ::_thesis: g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> thus g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) by Th14 .= g . ((g . (d2,d1)),d3) by A1, BINOP_1:def_2 .= g "**" <*d2,d1,d3*> by Th14 ; ::_thesis: verum end; theorem Th16: :: FINSOP_1:16 for D being non empty set for d being Element of D for g being BinOp of D holds g "**" (1 |-> d) = d proof let D be non empty set ; ::_thesis: for d being Element of D for g being BinOp of D holds g "**" (1 |-> d) = d let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" (1 |-> d) = d let g be BinOp of D; ::_thesis: g "**" (1 |-> d) = d thus g "**" (1 |-> d) = g "**" <*d*> by FINSEQ_2:59 .= d by Lm4 ; ::_thesis: verum end; theorem :: FINSOP_1:17 for D being non empty set for d being Element of D for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d) proof let D be non empty set ; ::_thesis: for d being Element of D for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d) let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d) let g be BinOp of D; ::_thesis: g "**" (2 |-> d) = g . (d,d) thus g "**" (2 |-> d) = g "**" <*d,d*> by FINSEQ_2:61 .= g . (d,d) by Th12 ; ::_thesis: verum end; theorem Th18: :: FINSOP_1:18 for D being non empty set for d being Element of D for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) proof let D be non empty set ; ::_thesis: for d being Element of D for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) let d be Element of D; ::_thesis: for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) let g be BinOp of D; ::_thesis: for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) let k, l be Element of NAT ; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) ) ( k <> 0 & l <> 0 implies ( len (k |-> d) <> 0 & len (l |-> d) <> 0 ) ) by CARD_1:def_7; then A1: ( k <> 0 & l <> 0 implies ( len (k |-> d) >= 1 & len (l |-> d) >= 1 ) ) by NAT_1:14; (k + l) |-> d = (k |-> d) ^ (l |-> d) by FINSEQ_2:123; hence ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) ) by A1, Th5; ::_thesis: verum end; theorem :: FINSOP_1:19 for D being non empty set for d being Element of D for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) proof let D be non empty set ; ::_thesis: for d being Element of D for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) let d be Element of D; ::_thesis: for g being BinOp of D for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) let g be BinOp of D; ::_thesis: for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) let k, l be Element of NAT ; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) ) defpred S1[ Element of NAT ] means for g being BinOp of D for k being Element of NAT for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & \$1 <> 0 ) ) holds g "**" ((k * \$1) |-> d) = g "**" (\$1 |-> (g "**" (k |-> d))); A1: for l being Element of NAT st S1[l] holds S1[l + 1] proof let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A2: S1[l] ; ::_thesis: S1[l + 1] let g be BinOp of D; ::_thesis: for k being Element of NAT for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) let k be Element of NAT ; ::_thesis: for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) let d be Element of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) implies g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) ) assume that A3: g is associative and A4: ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) now__::_thesis:_g_"**"_((k_*_(l_+_1))_|->_d)_=_g_"**"_((l_+_1)_|->_(g_"**"_(k_|->_d))) percases ( l = 0 or l <> 0 ) ; suppose l = 0 ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by Th16; ::_thesis: verum end; supposeA5: l <> 0 ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) then A6: ( k <> 0 implies k * l <> 0 ) by XCMPLX_1:6; g "**" ((k * (l + 1)) |-> d) = g "**" (((k * l) + (k * 1)) |-> d) .= g . ((g "**" ((k * l) |-> d)),(g "**" (k |-> d))) by A3, A4, A6, Th18 .= g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (k |-> d))) by A2, A3, A4, A5 .= g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (1 |-> (g "**" (k |-> d))))) by Th16 ; hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by A3, A5, Th18; ::_thesis: verum end; end; end; hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) ; ::_thesis: verum end; A7: S1[ 0 ] ; for l being Element of NAT holds S1[l] from NAT_1:sch_1(A7, A1); hence ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) ) ; ::_thesis: verum end; theorem :: FINSOP_1:20 for D being non empty set for F being FinSequence of D for g being BinOp of D st len F = 1 holds g "**" F = F . 1 by Lm11; theorem :: FINSOP_1:21 for D being non empty set for F being FinSequence of D for g being BinOp of D st len F = 2 holds g "**" F = g . ((F . 1),(F . 2)) proof let D be non empty set ; ::_thesis: for F being FinSequence of D for g being BinOp of D st len F = 2 holds g "**" F = g . ((F . 1),(F . 2)) let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 2 holds g "**" F = g . ((F . 1),(F . 2)) let g be BinOp of D; ::_thesis: ( len F = 2 implies g "**" F = g . ((F . 1),(F . 2)) ) assume A1: len F = 2 ; ::_thesis: g "**" F = g . ((F . 1),(F . 2)) then F = <*(F . 1),(F . 2)*> by FINSEQ_1:44 .= <*(F /. 1),(F . 2)*> by A1, FINSEQ_4:15 .= <*(F /. 1),(F /. 2)*> by A1, FINSEQ_4:15 ; hence g "**" F = g . ((F /. 1),(F /. 2)) by Th12 .= g . ((F . 1),(F /. 2)) by A1, FINSEQ_4:15 .= g . ((F . 1),(F . 2)) by A1, FINSEQ_4:15 ; ::_thesis: verum end;