:: AFINSQ_2 semantic presentation begin Lm1: for X, Y being finite set st X c= Y & card X = card Y holds X = Y proof let X, Y be finite set ; ::_thesis: ( X c= Y & card X = card Y implies X = Y ) assume that A1: X c= Y and A2: card X = card Y ; ::_thesis: X = Y card (Y \ X) = (card Y) - (card X) by A1, CARD_2:44; then Y \ X = {} by A2; then Y c= X by XBOOLE_1:37; hence X = Y by A1, XBOOLE_0:def_10; ::_thesis: verum end; Lm2: for X, Y being finite set for F being Function of X,Y st card X = card Y holds ( F is onto iff F is one-to-one ) proof let X, Y be finite set ; ::_thesis: for F being Function of X,Y st card X = card Y holds ( F is onto iff F is one-to-one ) let F be Function of X,Y; ::_thesis: ( card X = card Y implies ( F is onto iff F is one-to-one ) ) assume A1: card X = card Y ; ::_thesis: ( F is onto iff F is one-to-one ) thus ( F is onto implies F is one-to-one ) ::_thesis: ( F is one-to-one implies F is onto ) proof assume A2: F is onto ; ::_thesis: F is one-to-one assume not F is one-to-one ; ::_thesis: contradiction then consider x1, x2 being set such that A3: x1 in dom F and A4: x2 in dom F and A5: F . x1 = F . x2 and A6: x1 <> x2 by FUNCT_1:def_4; reconsider Xx = X \ {x1} as finite set ; Y c= F .: Xx proof let Fy be set ; :: according to TARSKI:def_3 ::_thesis: ( not Fy in Y or Fy in F .: Xx ) assume Fy in Y ; ::_thesis: Fy in F .: Xx then Fy in rng F by A2, FUNCT_2:def_3; then consider y being set such that A7: y in dom F and A8: F . y = Fy by FUNCT_1:def_3; now__::_thesis:_Fy_in_F_.:_Xx percases ( y = x1 or y <> x1 ) ; supposeA9: y = x1 ; ::_thesis: Fy in F .: Xx x2 in Xx by A4, A6, ZFMISC_1:56; hence Fy in F .: Xx by A4, A5, A8, A9, FUNCT_1:def_6; ::_thesis: verum end; suppose y <> x1 ; ::_thesis: Fy in F .: Xx then y in Xx by A7, ZFMISC_1:56; hence Fy in F .: Xx by A7, A8, FUNCT_1:def_6; ::_thesis: verum end; end; end; hence Fy in F .: Xx ; ::_thesis: verum end; then A10: card Y c= card Xx by CARD_1:66; {x1} meets X by A3, ZFMISC_1:48; then A11: Xx <> X by XBOOLE_1:83; Xx c< X by A11, XBOOLE_0:def_8; then card Xx < card X by CARD_2:48; hence contradiction by A1, A10, NAT_1:39; ::_thesis: verum end; thus ( F is one-to-one implies F is onto ) ::_thesis: verum proof assume F is one-to-one ; ::_thesis: F is onto then dom F,F .: (dom F) are_equipotent by CARD_1:33; then A12: card (dom F) = card (F .: (dom F)) by CARD_1:5; assume not F is onto ; ::_thesis: contradiction then not rng F = Y by FUNCT_2:def_3; then not Y c= rng F by XBOOLE_0:def_10; then consider y being set such that A13: y in Y and A14: not y in rng F by TARSKI:def_3; A15: card (rng F) <= card (Y \ {y}) by A14, NAT_1:43, ZFMISC_1:34; A16: F .: (dom F) = rng F by RELAT_1:113; {y} meets Y by A13, ZFMISC_1:48; then A17: Y \ {y} <> Y by XBOOLE_1:83; Y \ {y} c< Y by A17, XBOOLE_0:def_8; then card (Y \ {y}) < card Y by CARD_2:48; hence contradiction by A1, A13, A15, A12, A16, FUNCT_2:def_1; ::_thesis: verum end; end; theorem Th1: :: AFINSQ_2:1 for i being Nat for x being set st x in i holds x is Element of NAT proof let i be Nat; ::_thesis: for x being set st x in i holds x is Element of NAT let x be set ; ::_thesis: ( x in i implies x is Element of NAT ) A1: i c= NAT ; assume x in i ; ::_thesis: x is Element of NAT hence x is Element of NAT by A1; ::_thesis: verum end; registration cluster natural -> natural-membered for set ; coherence for b1 being Nat holds b1 is natural-membered proof let n be Nat; ::_thesis: n is natural-membered for x being set st x in n holds x is natural by Th1; hence n is natural-membered by MEMBERED:def_6; ::_thesis: verum end; end; begin theorem Th2: :: AFINSQ_2:2 for X0 being finite natural-membered set ex n being Nat st X0 c= n proof let X0 be finite natural-membered set ; ::_thesis: ex n being Nat st X0 c= n consider p being Function such that A1: rng p = X0 and A2: dom p in NAT by FINSET_1:def_1; reconsider np = dom p as Element of NAT by A2; np = dom p ; then reconsider p = p as XFinSequence by AFINSQ_1:5; X0 c= NAT by MEMBERED:6; then reconsider p = p as XFinSequence of NAT by A1, RELAT_1:def_19; defpred S1[ Nat] means ex n being Nat st for i being Nat st i in $1 & $1 -' 1 in dom p holds p . i in n; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then consider n being Nat such that A4: for i being Nat st i in k & k -' 1 in dom p holds p . i in n ; percases ( (k + 1) - 1 < len p or (k + 1) - 1 >= len p ) ; supposeA5: (k + 1) - 1 < len p ; ::_thesis: S1[k + 1] set m = p . k; set m2 = max (n,((p . k) + 1)); k -' 1 <= k by NAT_D:35; then k -' 1 < len p by A5, XXREAL_0:2; then A6: k -' 1 in dom p by NAT_1:44; for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds p . i in max (n,((p . k) + 1)) proof let i be Nat; ::_thesis: ( i in k + 1 & (k + 1) -' 1 in dom p implies p . i in max (n,((p . k) + 1)) ) assume that A7: i in k + 1 and (k + 1) -' 1 in dom p ; ::_thesis: p . i in max (n,((p . k) + 1)) A8: i < k + 1 by A7, NAT_1:44; percases ( i < k or i >= k ) ; supposeA9: i < k ; ::_thesis: p . i in max (n,((p . k) + 1)) set k0 = p . i; i in k by A9, NAT_1:44; then p . i in n by A4, A6; then p . i < n by NAT_1:44; then p . i < max (n,((p . k) + 1)) by XXREAL_0:30; hence p . i in max (n,((p . k) + 1)) by NAT_1:44; ::_thesis: verum end; supposeA10: i >= k ; ::_thesis: p . i in max (n,((p . k) + 1)) p . k < (p . k) + 1 by XREAL_1:29; then A11: p . k < max (n,((p . k) + 1)) by XXREAL_0:30; i <= k by A8, NAT_1:13; then p . i = p . k by A10, XXREAL_0:1; hence p . i in max (n,((p . k) + 1)) by A11, NAT_1:44; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; supposeA12: (k + 1) - 1 >= len p ; ::_thesis: S1[k + 1] (k + 1) -' 1 = k by NAT_D:34; then for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds p . i in 2 by A12, NAT_1:44; hence S1[k + 1] ; ::_thesis: verum end; end; end; for i being Nat st i in 0 & 0 -' 1 in dom p holds p . i in 0 ; then A13: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3); then consider n being Nat such that A14: for i being Nat st i in len p & (len p) -' 1 in dom p holds p . i in n ; rng p c= n proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in n ) assume y in rng p ; ::_thesis: y in n then consider x being set such that A15: x in dom p and A16: y = p . x by FUNCT_1:def_3; A17: (len p) - 1 < len p by XREAL_1:44; 0 + 1 <= len p by A15, NAT_1:13; then (len p) -' 1 = (len p) - 1 by XREAL_1:233; then (len p) -' 1 in dom p by A17, NAT_1:44; hence y in n by A14, A15, A16; ::_thesis: verum end; hence ex n being Nat st X0 c= n by A1; ::_thesis: verum end; theorem Th3: :: AFINSQ_2:3 for x being set for p being XFinSequence st x in rng p holds ex i being Element of NAT st ( i in dom p & p . i = x ) proof let x be set ; ::_thesis: for p being XFinSequence st x in rng p holds ex i being Element of NAT st ( i in dom p & p . i = x ) let p be XFinSequence; ::_thesis: ( x in rng p implies ex i being Element of NAT st ( i in dom p & p . i = x ) ) assume x in rng p ; ::_thesis: ex i being Element of NAT st ( i in dom p & p . i = x ) then ex a being set st ( a in dom p & x = p . a ) by FUNCT_1:def_3; hence ex i being Element of NAT st ( i in dom p & p . i = x ) ; ::_thesis: verum end; theorem Th4: :: AFINSQ_2:4 for D being set for p being XFinSequence st ( for i being Nat st i in dom p holds p . i in D ) holds p is XFinSequence of D proof let D be set ; ::_thesis: for p being XFinSequence st ( for i being Nat st i in dom p holds p . i in D ) holds p is XFinSequence of D let p be XFinSequence; ::_thesis: ( ( for i being Nat st i in dom p holds p . i in D ) implies p is XFinSequence of D ) assume A1: for i being Nat st i in dom p holds p . i in D ; ::_thesis: p is XFinSequence of D rng p c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in D ) assume x in rng p ; ::_thesis: x in D then ex i being Element of NAT st ( i in dom p & p . i = x ) by Th3; hence x in D by A1; ::_thesis: verum end; hence p is XFinSequence of D by RELAT_1:def_19; ::_thesis: verum end; scheme :: AFINSQ_2:sch 1 XSeqLambdaD{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } : ex p being XFinSequence of F2() st ( len p = F1() & ( for j being Nat st j in F1() holds p . j = F3(j) ) ) proof consider z being XFinSequence such that A1: len z = F1() and A2: for i being Nat st i in F1() holds z . i = F3(i) from AFINSQ_1:sch_2(); for j being Nat st j in F1() holds z . j in F2() proof let j be Nat; ::_thesis: ( j in F1() implies z . j in F2() ) reconsider j0 = j as Element of NAT by ORDINAL1:def_12; assume j in F1() ; ::_thesis: z . j in F2() then z . j0 = F3(j0) by A2; hence z . j in F2() ; ::_thesis: verum end; then reconsider z = z as XFinSequence of F2() by A1, Th4; take z ; ::_thesis: ( len z = F1() & ( for j being Nat st j in F1() holds z . j = F3(j) ) ) thus len z = F1() by A1; ::_thesis: for j being Nat st j in F1() holds z . j = F3(j) let j be Nat; ::_thesis: ( j in F1() implies z . j = F3(j) ) thus ( j in F1() implies z . j = F3(j) ) by A2; ::_thesis: verum end; registration cluster Relation-like NAT -defined Function-like empty T-Sequence-like natural-valued finite V86() for set ; existence ex b1 being XFinSequence st ( b1 is empty & b1 is natural-valued ) proof take the empty XFinSequence of NAT ; ::_thesis: ( the empty XFinSequence of NAT is empty & the empty XFinSequence of NAT is natural-valued ) thus ( the empty XFinSequence of NAT is empty & the empty XFinSequence of NAT is natural-valued ) ; ::_thesis: verum end; let p be T-Sequence-like complex-valued Function; cluster - p -> T-Sequence-like ; coherence - p is T-Sequence-like proof ( dom p = dom (- p) & dom p is ordinal ) by VALUED_1:8; hence - p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; clusterp " -> T-Sequence-like ; coherence p " is T-Sequence-like proof dom p = dom (p ") by VALUED_1:def_7; hence p " is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; clusterp ^2 -> T-Sequence-like ; coherence p ^2 is T-Sequence-like proof dom p = dom (p ^2) by VALUED_1:11; hence p ^2 is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; cluster|.p.| -> T-Sequence-like ; coherence abs p is T-Sequence-like proof dom p = dom (abs p) by VALUED_1:def_11; hence abs p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; let q be T-Sequence-like complex-valued Function; clusterp + q -> T-Sequence-like ; coherence p + q is T-Sequence-like proof ( dom (p + q) = (dom p) /\ (dom q) & dom p is ordinal & dom q is ordinal ) by VALUED_1:def_1; hence p + q is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; clusterp - q -> T-Sequence-like ; coherence p - q is T-Sequence-like ; clusterp (#) q -> T-Sequence-like ; coherence p (#) q is T-Sequence-like proof ( dom (p (#) q) = (dom p) /\ (dom q) & dom p is ordinal & dom q is ordinal ) by VALUED_1:def_4; hence p (#) q is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; clusterp /" q -> T-Sequence-like ; coherence p /" q is T-Sequence-like ; end; registration let p be complex-valued finite Function; cluster - p -> finite ; coherence - p is finite proof dom p = dom (- p) by VALUED_1:8; hence - p is finite by FINSET_1:10; ::_thesis: verum end; clusterp " -> finite ; coherence p " is finite proof dom p = dom (p ") by VALUED_1:def_7; hence p " is finite by FINSET_1:10; ::_thesis: verum end; clusterp ^2 -> finite ; coherence p ^2 is finite proof dom p = dom (p ^2) by VALUED_1:11; hence p ^2 is finite by FINSET_1:10; ::_thesis: verum end; cluster|.p.| -> finite ; coherence abs p is finite proof dom p = dom (abs p) by VALUED_1:def_11; hence abs p is finite by FINSET_1:10; ::_thesis: verum end; let q be complex-valued Function; clusterp + q -> finite ; coherence p + q is finite proof dom (p + q) = (dom p) /\ (dom q) by VALUED_1:def_1; hence p + q is finite by FINSET_1:10; ::_thesis: verum end; clusterp - q -> finite ; coherence p - q is finite ; clusterp (#) q -> finite ; coherence p (#) q is finite proof dom (p (#) q) = (dom p) /\ (dom q) by VALUED_1:def_4; hence p (#) q is finite by FINSET_1:10; ::_thesis: verum end; clusterp /" q -> finite ; coherence p /" q is finite ; clusterq /" p -> finite ; coherence q /" p is finite ; end; registration let p be T-Sequence-like complex-valued Function; let c be complex number ; clusterc + p -> T-Sequence-like ; coherence c + p is T-Sequence-like proof dom p = dom (c + p) by VALUED_1:def_2; hence c + p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; clusterp - c -> T-Sequence-like ; coherence p - c is T-Sequence-like ; clusterc (#) p -> T-Sequence-like ; coherence c (#) p is T-Sequence-like proof dom p = dom (c (#) p) by VALUED_1:def_5; hence c (#) p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum end; end; registration let p be complex-valued finite Function; let c be complex number ; clusterc + p -> finite ; coherence c + p is finite proof dom p = dom (c + p) by VALUED_1:def_2; hence c + p is finite by FINSET_1:10; ::_thesis: verum end; clusterp - c -> finite ; coherence p - c is finite ; clusterc (#) p -> finite ; coherence c (#) p is finite proof dom p = dom (c (#) p) by VALUED_1:def_5; hence c (#) p is finite by FINSET_1:10; ::_thesis: verum end; end; definition let p be XFinSequence; func Rev p -> XFinSequence means :Def1: :: AFINSQ_2:def 1 ( len it = len p & ( for i being Nat st i in dom it holds it . i = p . ((len p) - (i + 1)) ) ); existence ex b1 being XFinSequence st ( len b1 = len p & ( for i being Nat st i in dom b1 holds b1 . i = p . ((len p) - (i + 1)) ) ) proof deffunc H1( Nat) -> set = p . ((len p) - ($1 + 1)); ex q being XFinSequence st ( len q = len p & ( for k being Nat st k in len p holds q . k = H1(k) ) ) from AFINSQ_1:sch_2(); hence ex b1 being XFinSequence st ( len b1 = len p & ( for i being Nat st i in dom b1 holds b1 . i = p . ((len p) - (i + 1)) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence st len b1 = len p & ( for i being Nat st i in dom b1 holds b1 . i = p . ((len p) - (i + 1)) ) & len b2 = len p & ( for i being Nat st i in dom b2 holds b2 . i = p . ((len p) - (i + 1)) ) holds b1 = b2 proof let f1, f2 be XFinSequence; ::_thesis: ( len f1 = len p & ( for i being Nat st i in dom f1 holds f1 . i = p . ((len p) - (i + 1)) ) & len f2 = len p & ( for i being Nat st i in dom f2 holds f2 . i = p . ((len p) - (i + 1)) ) implies f1 = f2 ) assume that A1: len f1 = len p and A2: for i being Nat st i in dom f1 holds f1 . i = p . ((len p) - (i + 1)) and A3: len f2 = len p and A4: for i being Nat st i in dom f2 holds f2 . i = p . ((len p) - (i + 1)) ; ::_thesis: f1 = f2 now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ f1_._i_=_f2_._i let i be Nat; ::_thesis: ( i in dom p implies f1 . i = f2 . i ) assume A5: i in dom p ; ::_thesis: f1 . i = f2 . i then f1 . i = p . ((len p) - (i + 1)) by A1, A2; hence f1 . i = f2 . i by A3, A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, AFINSQ_1:8; ::_thesis: verum end; end; :: deftheorem Def1 defines Rev AFINSQ_2:def_1_:_ for p, b2 being XFinSequence holds ( b2 = Rev p iff ( len b2 = len p & ( for i being Nat st i in dom b2 holds b2 . i = p . ((len p) - (i + 1)) ) ) ); theorem Th5: :: AFINSQ_2:5 for p being XFinSequence holds ( dom p = dom (Rev p) & rng p = rng (Rev p) ) proof let p be XFinSequence; ::_thesis: ( dom p = dom (Rev p) & rng p = rng (Rev p) ) thus A1: dom p = len p .= len (Rev p) by Def1 .= dom (Rev p) ; ::_thesis: rng p = rng (Rev p) A2: len p = len (Rev p) by Def1; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng (Rev p) c= rng p let x be set ; ::_thesis: ( x in rng p implies x in rng (Rev p) ) assume x in rng p ; ::_thesis: x in rng (Rev p) then consider z being set such that A3: z in dom p and A4: p . z = x by FUNCT_1:def_3; reconsider i = z as Element of NAT by A3; i < len p by A3, NAT_1:44; then i + 1 <= len p by NAT_1:13; then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233; then reconsider j = (len p) - (i + 1) as Element of NAT ; (len p) - (i + 1) < len p by XREAL_1:44; then A5: j in len (Rev p) by A2, NAT_1:44; then (Rev p) . j = p . ((len p) - (j + 1)) by Def1; hence x in rng (Rev p) by A4, A5, FUNCT_1:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rev p) or x in rng p ) assume x in rng (Rev p) ; ::_thesis: x in rng p then consider z being set such that A6: z in dom (Rev p) and A7: (Rev p) . z = x by FUNCT_1:def_3; reconsider i = z as Element of NAT by A6; i < len p by A2, A6, NAT_1:44; then i + 1 <= len p by NAT_1:13; then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233; then reconsider j = (len p) - (i + 1) as Element of NAT ; (len p) - (i + 1) < len p by XREAL_1:44; then A8: j in len (Rev p) by A2, NAT_1:44; (Rev p) . i = p . ((len p) - (i + 1)) by A6, Def1; hence x in rng p by A1, A7, A8, FUNCT_1:def_3; ::_thesis: verum end; registration let D be set ; let f be XFinSequence of D; cluster Rev f -> D -valued ; coherence Rev f is D -valued proof rng f = rng (Rev f) by Th5; hence Rev f is D -valued by RELAT_1:def_19; ::_thesis: verum end; end; definition let p be XFinSequence; let n be Nat; funcp /^ n -> XFinSequence means :Def2: :: AFINSQ_2:def 2 ( len it = (len p) -' n & ( for m being Nat st m in dom it holds it . m = p . (m + n) ) ); existence ex b1 being XFinSequence st ( len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds b1 . m = p . (m + n) ) ) proof thus ex p1 being XFinSequence st ( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds p1 . m = p . (m + n) ) ) ::_thesis: verum proof deffunc H1( Nat) -> set = p . ($1 + n); set k = (len p) -' n; consider q being XFinSequence such that A1: ( len q = (len p) -' n & ( for m2 being Nat st m2 in (len p) -' n holds q . m2 = H1(m2) ) ) from AFINSQ_1:sch_2(); take q ; ::_thesis: ( len q = (len p) -' n & ( for m being Nat st m in dom q holds q . m = p . (m + n) ) ) thus ( len q = (len p) -' n & ( for m being Nat st m in dom q holds q . m = p . (m + n) ) ) by A1; ::_thesis: verum end; end; uniqueness for b1, b2 being XFinSequence st len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds b1 . m = p . (m + n) ) & len b2 = (len p) -' n & ( for m being Nat st m in dom b2 holds b2 . m = p . (m + n) ) holds b1 = b2 proof let p1, p2 be XFinSequence; ::_thesis: ( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds p1 . m = p . (m + n) ) & len p2 = (len p) -' n & ( for m being Nat st m in dom p2 holds p2 . m = p . (m + n) ) implies p1 = p2 ) thus ( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds p1 . m = p . (m + n) ) & len p2 = (len p) -' n & ( for m being Nat st m in dom p2 holds p2 . m = p . (m + n) ) implies p1 = p2 ) ::_thesis: verum proof assume that A2: len p1 = (len p) -' n and A3: for m being Nat st m in dom p1 holds p1 . m = p . (m + n) and A4: len p2 = (len p) -' n and A5: for m being Nat st m in dom p2 holds p2 . m = p . (m + n) ; ::_thesis: p1 = p2 now__::_thesis:_for_m_being_Nat_st_m_in_dom_p1_holds_ p1_._m_=_p2_._m let m be Nat; ::_thesis: ( m in dom p1 implies p1 . m = p2 . m ) assume A6: m in dom p1 ; ::_thesis: p1 . m = p2 . m then p1 . m = p . (m + n) by A3; hence p1 . m = p2 . m by A2, A4, A5, A6; ::_thesis: verum end; hence p1 = p2 by A2, A4, AFINSQ_1:8; ::_thesis: verum end; end; end; :: deftheorem Def2 defines /^ AFINSQ_2:def_2_:_ for p being XFinSequence for n being Nat for b3 being XFinSequence holds ( b3 = p /^ n iff ( len b3 = (len p) -' n & ( for m being Nat st m in dom b3 holds b3 . m = p . (m + n) ) ) ); theorem Th6: :: AFINSQ_2:6 for n being Nat for p being XFinSequence st n >= len p holds p /^ n = {} proof let n be Nat; ::_thesis: for p being XFinSequence st n >= len p holds p /^ n = {} let p be XFinSequence; ::_thesis: ( n >= len p implies p /^ n = {} ) assume n >= len p ; ::_thesis: p /^ n = {} then (len p) -' n = 0 by NAT_2:8; then len (p /^ n) = 0 by Def2; hence p /^ n = {} ; ::_thesis: verum end; theorem Th7: :: AFINSQ_2:7 for n being Nat for p being XFinSequence st n < len p holds len (p /^ n) = (len p) - n proof let n be Nat; ::_thesis: for p being XFinSequence st n < len p holds len (p /^ n) = (len p) - n let p be XFinSequence; ::_thesis: ( n < len p implies len (p /^ n) = (len p) - n ) assume n < len p ; ::_thesis: len (p /^ n) = (len p) - n then (len p) - n >= 0 by XREAL_1:48; then (len p) -' n = (len p) - n by XREAL_0:def_2; hence len (p /^ n) = (len p) - n by Def2; ::_thesis: verum end; theorem Th8: :: AFINSQ_2:8 for m, n being Nat for p being XFinSequence st m + n < len p holds (p /^ n) . m = p . (m + n) proof let m, n be Nat; ::_thesis: for p being XFinSequence st m + n < len p holds (p /^ n) . m = p . (m + n) let p be XFinSequence; ::_thesis: ( m + n < len p implies (p /^ n) . m = p . (m + n) ) assume A1: m + n < len p ; ::_thesis: (p /^ n) . m = p . (m + n) then A2: m < (len p) - n by XREAL_1:20; len (p /^ n) = (len p) - n by A1, Th7, NAT_1:12; then m in dom (p /^ n) by A2, NAT_1:44; hence (p /^ n) . m = p . (m + n) by Def2; ::_thesis: verum end; registration let f be one-to-one XFinSequence; let n be Nat; clusterf /^ n -> one-to-one ; coherence f /^ n is one-to-one proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom (f /^ n) or not y in dom (f /^ n) or not (f /^ n) . x = (f /^ n) . y or x = y ) assume that A1: x in dom (f /^ n) and A2: y in dom (f /^ n) and A3: (f /^ n) . x = (f /^ n) . y ; ::_thesis: x = y reconsider nx = x, ny = y as Nat by A1, A2; A4: nx < len (f /^ n) by A1, NAT_1:44; A5: len (f /^ n) = (len f) -' n by Def2; A6: ny < len (f /^ n) by A2, NAT_1:44; percases ( n <= len f or n > len f ) ; suppose n <= len f ; ::_thesis: x = y then A7: (len f) -' n = (len f) - n by XREAL_1:233; then A8: nx + n < len f by A4, A5, XREAL_1:20; then A9: nx + n in dom f by NAT_1:44; A10: ny + n < len f by A6, A5, A7, XREAL_1:20; then A11: ny + n in dom f by NAT_1:44; A12: (f /^ n) . ny = f . (ny + n) by A10, Th8; (f /^ n) . nx = f . (nx + n) by A8, Th8; then nx + n = ny + n by A3, A9, A12, A11, FUNCT_1:def_4; hence x = y ; ::_thesis: verum end; suppose n > len f ; ::_thesis: x = y then f /^ n = {} by Th6; hence x = y by A1; ::_thesis: verum end; end; end; end; theorem Th9: :: AFINSQ_2:9 for n being Nat for p being XFinSequence holds rng (p /^ n) c= rng p proof let n be Nat; ::_thesis: for p being XFinSequence holds rng (p /^ n) c= rng p let p be XFinSequence; ::_thesis: rng (p /^ n) c= rng p thus rng (p /^ n) c= rng p ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (p /^ n) or z in rng p ) assume z in rng (p /^ n) ; ::_thesis: z in rng p then consider x being set such that A1: x in dom (p /^ n) and A2: z = (p /^ n) . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A1; nx < len (p /^ n) by A1, NAT_1:44; then A3: nx < (len p) -' n by Def2; percases ( n < len p or n >= len p ) ; suppose n < len p ; ::_thesis: z in rng p then (len p) -' n = (len p) - n by XREAL_1:233; then nx + n < len p by A3, XREAL_1:20; then A4: nx + n in dom p by NAT_1:44; (p /^ n) . nx = p . (nx + n) by A1, Def2; hence z in rng p by A2, A4, FUNCT_1:def_3; ::_thesis: verum end; suppose n >= len p ; ::_thesis: z in rng p then p /^ n = {} by Th6; hence z in rng p by A1; ::_thesis: verum end; end; end; end; theorem Th10: :: AFINSQ_2:10 for p being XFinSequence holds p /^ 0 = p proof let p be XFinSequence; ::_thesis: p /^ 0 = p percases ( 0 < len p or 0 >= len p ) ; supposeA1: 0 < len p ; ::_thesis: p /^ 0 = p A2: now__::_thesis:_for_i_being_Nat_st_i_<_len_(p_/^_0)_holds_ (p_/^_0)_._i_=_p_._i let i be Nat; ::_thesis: ( i < len (p /^ 0) implies (p /^ 0) . i = p . i ) assume i < len (p /^ 0) ; ::_thesis: (p /^ 0) . i = p . i then i in dom (p /^ 0) by NAT_1:44; hence (p /^ 0) . i = p . (i + 0) by Def2 .= p . i ; ::_thesis: verum end; len (p /^ 0) = (len p) - 0 by A1, Th7 .= len p ; hence p /^ 0 = p by A2, AFINSQ_1:9; ::_thesis: verum end; supposeA3: 0 >= len p ; ::_thesis: p /^ 0 = p then p /^ 0 = {} by Th6; hence p /^ 0 = p by A3; ::_thesis: verum end; end; end; theorem Th11: :: AFINSQ_2:11 for i being Nat for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i proof let i be Nat; ::_thesis: for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i let p, q be XFinSequence; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i A1: len (p ^ q) = (len p) + (len q) by AFINSQ_1:17; percases ( i < len q or i >= len q ) ; supposeA2: i < len q ; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i then (len p) + i < (len p) + (len q) by XREAL_1:6; then (len p) + i < len (p ^ q) by AFINSQ_1:17; then A3: len ((p ^ q) /^ ((len p) + i)) = (len (p ^ q)) - ((len p) + i) by Th7 .= ((len q) + (len p)) - ((len p) + i) by AFINSQ_1:17 .= (len q) - i .= len (q /^ i) by A2, Th7 ; now__::_thesis:_for_k_being_Nat_st_k_<_len_(q_/^_i)_holds_ ((p_^_q)_/^_((len_p)_+_i))_._k_=_(q_/^_i)_._k let k be Nat; ::_thesis: ( k < len (q /^ i) implies ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k ) assume A4: k < len (q /^ i) ; ::_thesis: ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k then A5: k in dom (q /^ i) by NAT_1:44; k < (len q) - i by A2, A4, Th7; then i + k < len q by XREAL_1:20; then A6: i + k in dom q by NAT_1:44; k in dom ((p ^ q) /^ ((len p) + i)) by A3, A4, NAT_1:44; hence ((p ^ q) /^ ((len p) + i)) . k = (p ^ q) . (((len p) + i) + k) by Def2 .= (p ^ q) . ((len p) + (i + k)) .= q . (i + k) by A6, AFINSQ_1:def_3 .= (q /^ i) . k by A5, Def2 ; ::_thesis: verum end; hence (p ^ q) /^ ((len p) + i) = q /^ i by A3, AFINSQ_1:9; ::_thesis: verum end; supposeA7: i >= len q ; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i then (len p) + i >= len (p ^ q) by A1, XREAL_1:6; hence (p ^ q) /^ ((len p) + i) = {} by Th6 .= q /^ i by A7, Th6 ; ::_thesis: verum end; end; end; theorem Th12: :: AFINSQ_2:12 for p, q being XFinSequence holds (p ^ q) /^ (len p) = q proof let p, q be XFinSequence; ::_thesis: (p ^ q) /^ (len p) = q thus (p ^ q) /^ (len p) = (p ^ q) /^ ((len p) + 0) .= q /^ 0 by Th11 .= q by Th10 ; ::_thesis: verum end; theorem :: AFINSQ_2:13 for n being Nat for p being XFinSequence holds (p | n) ^ (p /^ n) = p proof let n be Nat; ::_thesis: for p being XFinSequence holds (p | n) ^ (p /^ n) = p let p be XFinSequence; ::_thesis: (p | n) ^ (p /^ n) = p set pn = p /^ n; now__::_thesis:_(_(_len_p_<=_n_&_(p_|_n)_^_(p_/^_n)_=_p_)_or_(_n_<_len_p_&_(p_|_n)_^_(p_/^_n)_=_p_)_) percases ( len p <= n or n < len p ) ; caseA1: len p <= n ; ::_thesis: (p | n) ^ (p /^ n) = p A2: p ^ {} = p ; p /^ n = {} by A1, Th6; hence (p | n) ^ (p /^ n) = p by A1, A2, AFINSQ_1:52; ::_thesis: verum end; caseA3: n < len p ; ::_thesis: (p | n) ^ (p /^ n) = p set g = p | n; A4: len (p | n) = n by A3, AFINSQ_1:54; A5: len (p /^ n) = (len p) - n by A3, Th7; A6: now__::_thesis:_for_m_being_Nat_st_m_<_len_p_holds_ ((p_|_n)_^_(p_/^_n))_._m_=_p_._m let m be Nat; ::_thesis: ( m < len p implies ((p | n) ^ (p /^ n)) . m = p . m ) assume A7: m < len p ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m now__::_thesis:_(_(_m_<_n_&_((p_|_n)_^_(p_/^_n))_._m_=_p_._m_)_or_(_n_<=_m_&_((p_|_n)_^_(p_/^_n))_._m_=_p_._m_)_) percases ( m < n or n <= m ) ; case m < n ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m then A8: m in n by NAT_1:44; hence ((p | n) ^ (p /^ n)) . m = (p | n) . m by A4, AFINSQ_1:def_3 .= p . m by A3, A8, AFINSQ_1:53 ; ::_thesis: verum end; case n <= m ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m then max (0,(m - n)) = m - n by FINSEQ_2:4; then reconsider k = m - n as Element of NAT by FINSEQ_2:5; k < len (p /^ n) by A5, A7, XREAL_1:9; then A9: k in dom (p /^ n) by NAT_1:44; m = (len (p | n)) + k by A4; hence ((p | n) ^ (p /^ n)) . m = (p /^ n) . k by A9, AFINSQ_1:def_3 .= p . (k + n) by A9, Def2 .= p . m ; ::_thesis: verum end; end; end; hence ((p | n) ^ (p /^ n)) . m = p . m ; ::_thesis: verum end; len ((p | n) ^ (p /^ n)) = n + ((len p) - n) by A5, A4, AFINSQ_1:17 .= len p ; hence (p | n) ^ (p /^ n) = p by A6, AFINSQ_1:9; ::_thesis: verum end; end; end; hence (p | n) ^ (p /^ n) = p ; ::_thesis: verum end; registration let D be set ; let f be XFinSequence of D; let n be Nat; clusterf /^ n -> D -valued ; coherence f /^ n is D -valued proof deffunc H1( Element of NAT ) -> set = f . (D + n); set p = f /^ n; percases ( n < len f or len f <= n ) ; supposeA1: n < len f ; ::_thesis: f /^ n is D -valued then reconsider k = (len f) - n as Nat by NAT_1:21; A2: len (f /^ n) = k by A1, Th7; A3: rng (f /^ n) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f /^ n) or x in rng f ) assume x in rng (f /^ n) ; ::_thesis: x in rng f then consider m being Element of NAT such that A4: m in dom (f /^ n) and A5: (f /^ n) . m = x by Th3; m < len (f /^ n) by A4, NAT_1:44; then m + n < k + n by A2, XREAL_1:6; then A6: m + n in dom f by NAT_1:44; (f /^ n) . m = f . (m + n) by A4, Def2; hence x in rng f by A5, A6, FUNCT_1:def_3; ::_thesis: verum end; for f2 being XFinSequence st rng f2 c= D holds f2 is XFinSequence of D by RELAT_1:def_19; hence f /^ n is D -valued by A3, XBOOLE_1:1; ::_thesis: verum end; suppose len f <= n ; ::_thesis: f /^ n is D -valued then f /^ n = <%> D by Th6; hence f /^ n is D -valued ; ::_thesis: verum end; end; end; end; definition let p be XFinSequence; let k1, k2 be Nat; func mid (p,k1,k2) -> XFinSequence equals :: AFINSQ_2:def 3 (p | k2) /^ (k1 -' 1); coherence (p | k2) /^ (k1 -' 1) is XFinSequence ; end; :: deftheorem defines mid AFINSQ_2:def_3_:_ for p being XFinSequence for k1, k2 being Nat holds mid (p,k1,k2) = (p | k2) /^ (k1 -' 1); theorem Th14: :: AFINSQ_2:14 for p being XFinSequence for k1, k2 being Nat st k1 > k2 holds mid (p,k1,k2) = {} proof let p be XFinSequence; ::_thesis: for k1, k2 being Nat st k1 > k2 holds mid (p,k1,k2) = {} let k1, k2 be Nat; ::_thesis: ( k1 > k2 implies mid (p,k1,k2) = {} ) set k21 = k2; A1: len (p | k2) <= k2 by AFINSQ_1:55; assume A2: k1 > k2 ; ::_thesis: mid (p,k1,k2) = {} then k1 >= 0 + 1 by NAT_1:13; then A3: k1 -' 1 = k1 - 1 by XREAL_1:233; k1 >= k2 + 1 by A2, NAT_1:13; then k1 - 1 >= (k2 + 1) - 1 by XREAL_1:9; hence mid (p,k1,k2) = {} by A3, A1, Th6, XXREAL_0:2; ::_thesis: verum end; theorem :: AFINSQ_2:15 for p being XFinSequence for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) proof let p be XFinSequence; ::_thesis: for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) let k1, k2 be Nat; ::_thesis: ( 1 <= k1 & k2 <= len p implies mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) ) assume that A1: 1 <= k1 and A2: k2 <= len p ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) set k11 = k1; set k21 = k2; A3: len (p | k2) = k2 by A2, AFINSQ_1:54; k1 < k1 + 1 by NAT_1:13; then k1 - 1 < (k1 + 1) - 1 by XREAL_1:9; then A4: k1 -' 1 < k1 by A1, XREAL_1:233; percases ( k1 <= k2 or k1 > k2 ) ; supposeA5: k1 <= k2 ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) A6: k2 < k2 + 1 by XREAL_1:29; then A7: (k2 + 1) -' k1 = (k2 + 1) - k1 by A5, XREAL_1:233, XXREAL_0:2 .= k2 - (k1 - 1) ; A8: k1 -' 1 = k1 - 1 by A1, XREAL_1:233; k1 - 1 < k1 by XREAL_1:44; then k1 - 1 < k2 by A5, XXREAL_0:2; then A9: len (mid (p,k1,k2)) = k2 - (k1 - 1) by A3, A8, Th7; then A10: len (mid (p,k1,k2)) = (k2 + 1) - k1 ; k1 -' 1 < k2 by A4, A5, XXREAL_0:2; then k1 -' 1 < len p by A2, XXREAL_0:2; then len (p /^ (k1 -' 1)) = (len p) - (k1 -' 1) by Th7; then A11: (k2 + 1) -' k1 <= len (p /^ (k1 -' 1)) by A2, A8, A7, XREAL_1:9; A12: for i being Nat st i < len (mid (p,k1,k2)) holds (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i proof let i be Nat; ::_thesis: ( i < len (mid (p,k1,k2)) implies (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i ) assume A13: i < len (mid (p,k1,k2)) ; ::_thesis: (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i then i + (k1 -' 1) < k2 by A8, A9, XREAL_1:20; then A14: i + (k1 -' 1) in k2 by NAT_1:44; i + (k1 -' 1) < (k2 - (k1 - 1)) + (k1 -' 1) by A9, A13, XREAL_1:6; then A15: i + (k1 -' 1) < len p by A2, A8, XXREAL_0:2; i + (k1 - 1) < k2 by A9, A13, XREAL_1:20; then A16: ((p | k2) /^ (k1 -' 1)) . i = (p | k2) . (i + (k1 -' 1)) by A3, A8, Th8; i in (k2 + 1) -' k1 by A7, A9, A13, NAT_1:44; then ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i = (p /^ (k1 -' 1)) . i by A11, AFINSQ_1:53 .= p . (i + (k1 -' 1)) by A15, Th8 ; hence (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i by A2, A16, A14, AFINSQ_1:53; ::_thesis: verum end; len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1 by A11, AFINSQ_1:54; then len (mid (p,k1,k2)) = len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) by A5, A6, A10, XREAL_1:233, XXREAL_0:2; hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A12, AFINSQ_1:9; ::_thesis: verum end; supposeA17: k1 > k2 ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) then k2 + 1 <= k1 by NAT_1:13; then A18: (k2 + 1) -' k1 = 0 by NAT_2:8; mid (p,k1,k2) = {} by A17, Th14; hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A18; ::_thesis: verum end; end; end; theorem Th16: :: AFINSQ_2:16 for k being Nat for p being XFinSequence holds mid (p,1,k) = p | k proof let k be Nat; ::_thesis: for p being XFinSequence holds mid (p,1,k) = p | k let p be XFinSequence; ::_thesis: mid (p,1,k) = p | k 1 -' 1 = 0 by XREAL_1:232; hence mid (p,1,k) = p | k by Th10; ::_thesis: verum end; theorem :: AFINSQ_2:17 for k being Nat for p being XFinSequence st len p <= k holds mid (p,1,k) = p proof let k be Nat; ::_thesis: for p being XFinSequence st len p <= k holds mid (p,1,k) = p let p be XFinSequence; ::_thesis: ( len p <= k implies mid (p,1,k) = p ) assume A1: len p <= k ; ::_thesis: mid (p,1,k) = p thus mid (p,1,k) = p | k by Th16 .= p by A1, AFINSQ_1:52 ; ::_thesis: verum end; theorem :: AFINSQ_2:18 for k being Nat for p being XFinSequence holds mid (p,0,k) = mid (p,1,k) proof let k be Nat; ::_thesis: for p being XFinSequence holds mid (p,0,k) = mid (p,1,k) let p be XFinSequence; ::_thesis: mid (p,0,k) = mid (p,1,k) A1: 0 -' 1 = 0 by NAT_2:8; mid (p,1,k) = p | k by Th16; hence mid (p,0,k) = mid (p,1,k) by A1, Th10; ::_thesis: verum end; theorem :: AFINSQ_2:19 for p, q being XFinSequence holds mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q proof let p, q be XFinSequence; ::_thesis: mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q A1: ((len p) + 1) -' 1 = len p by NAT_D:34; len (p ^ q) = (len p) + (len q) by AFINSQ_1:17; then (p ^ q) | ((len p) + (len q)) = p ^ q by AFINSQ_1:52; hence mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q by A1, Th12; ::_thesis: verum end; registration let D be set ; let f be XFinSequence of D; let k1, k2 be Nat; cluster mid (f,k1,k2) -> D -valued ; coherence mid (f,k1,k2) is D -valued ; end; begin definition let X be finite natural-membered set ; func Sgm0 X -> XFinSequence of NAT means :Def4: :: AFINSQ_2:def 4 ( rng it = X & ( for l, m, k1, k2 being Nat st l < m & m < len it & k1 = it . l & k2 = it . m holds k1 < k2 ) ); existence ex b1 being XFinSequence of NAT st ( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds k1 < k2 ) ) proof defpred S1[ Nat] means for X being set st X c= $1 holds ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ); A1: ex k being Nat st X c= k by Th2; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: for X being set st X c= k holds ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) ; ::_thesis: S1[k + 1] let X be set ; ::_thesis: ( X c= k + 1 implies ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) ) assume A4: X c= k + 1 ; ::_thesis: ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) now__::_thesis:_(_not_X_c=_k_implies_ex_p_being_XFinSequence_of_NAT_st_ (_rng_p_=_X_&_(_for_l,_m,_k1,_k2_being_Nat_st_l_<_m_&_m_<_len_p_&_k1_=_p_._l_&_k2_=_p_._m_holds_ k1_<_k2_)_)_) set Y = X \ {k}; assume not X c= k ; ::_thesis: ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) then consider x being set such that A5: x in X and A6: not x in k by TARSKI:def_3; reconsider n = x as Element of NAT by A4, A5, Th1; n < k + 1 by A4, A5, NAT_1:44; then A7: n <= k by NAT_1:13; not n < k by A6, NAT_1:44; then A8: n = k by A7, XXREAL_0:1; A9: X \ {k} c= k proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ {k} or x in k ) assume A10: x in X \ {k} ; ::_thesis: x in k then A11: x in X ; then reconsider m = x as Element of NAT by A4, Th1; not x in {k} by A10, XBOOLE_0:def_5; then A12: m <> k by TARSKI:def_1; m < k + 1 by A4, A11, NAT_1:44; then m <= k by NAT_1:13; then m < k by A12, XXREAL_0:1; hence x in k by NAT_1:44; ::_thesis: verum end; then consider p being XFinSequence of NAT such that A13: rng p = X \ {k} and A14: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 by A3; reconsider k = k as Element of NAT by ORDINAL1:def_12; consider q being XFinSequence of NAT such that A15: q = p ^ <%k%> ; A16: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 proof let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len q & k1 = q . l & k2 = q . m implies k1 < k2 ) assume that A17: l < m and A18: m < len q and A19: k1 = q . l and A20: k2 = q . m ; ::_thesis: k1 < k2 m + 1 <= len q by A18, NAT_1:13; then A21: m <= (len q) - 1 by XREAL_1:19; then l < (len (p ^ <%k%>)) - 1 by A15, A17, XXREAL_0:2; then l < ((len p) + (len <%k%>)) - 1 by AFINSQ_1:17; then l < ((len p) + 1) - 1 by AFINSQ_1:34; then A22: l in dom p by NAT_1:44; A23: m <= (len q) -' 1 by A21, XREAL_0:def_2; A24: now__::_thesis:_(_m_<>_(len_q)_-'_1_implies_k1_<_k2_) A25: k1 = p . l by A15, A19, A22, AFINSQ_1:def_3; assume m <> (len q) -' 1 ; ::_thesis: k1 < k2 then m < (len (p ^ <%k%>)) -' 1 by A15, A23, XXREAL_0:1; then m < ((len p) + (len <%k%>)) -' 1 by AFINSQ_1:17; then m < ((len p) + 1) -' 1 by AFINSQ_1:34; then A26: m < len p by NAT_D:34; then m in dom p by NAT_1:44; then k2 = p . m by A15, A20, AFINSQ_1:def_3; hence k1 < k2 by A14, A17, A26, A25; ::_thesis: verum end; now__::_thesis:_(_m_=_(len_q)_-'_1_implies_k1_<_k2_) assume m = (len q) -' 1 ; ::_thesis: k1 < k2 then A27: q . m = (p ^ <%k%>) . (((len p) + (len <%k%>)) -' 1) by A15, AFINSQ_1:17 .= (p ^ <%k%>) . (((len p) + 1) -' 1) by AFINSQ_1:34 .= (p ^ <%k%>) . (len p) by NAT_D:34 .= k by AFINSQ_1:36 ; k1 = p . l by A15, A19, A22, AFINSQ_1:def_3; then k1 in X \ {k} by A13, A22, FUNCT_1:def_3; hence k1 < k2 by A9, A20, A27, NAT_1:44; ::_thesis: verum end; hence k1 < k2 by A24; ::_thesis: verum end; A28: {k} c= X by A5, A8, ZFMISC_1:31; rng q = (rng p) \/ (rng <%k%>) by A15, AFINSQ_1:26 .= (X \ {k}) \/ {k} by A13, AFINSQ_1:33 .= X \/ {k} by XBOOLE_1:39 .= X by A28, XBOOLE_1:12 ; hence ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) by A16; ::_thesis: verum end; hence ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) by A3; ::_thesis: verum end; A29: S1[ 0 ] proof let X be set ; ::_thesis: ( X c= 0 implies ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) ) assume A30: X c= 0 ; ::_thesis: ex p being XFinSequence of NAT st ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) ) take <%> NAT ; ::_thesis: ( rng (<%> NAT) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds k1 < k2 ) ) thus rng (<%> NAT) = X by A30; ::_thesis: for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds k1 < k2 thus for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds k1 < k2 ; ::_thesis: verum end; for k2 being Nat holds S1[k2] from NAT_1:sch_2(A29, A2); hence ex b1 being XFinSequence of NAT st ( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds k1 < k2 ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds k1 < k2 ) holds b1 = b2 proof defpred S1[ XFinSequence] means for X being set st ex k being Nat st X c= k & $1 is XFinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len $1 & k1 = $1 . l & k2 = $1 . m holds k1 < k2 ) holds for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) holds q = $1; let p, q be XFinSequence of NAT ; ::_thesis: ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 ) & rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) implies p = q ) assume that A31: rng p = X and A32: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 and A33: rng q = X and A34: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ; ::_thesis: p = q A35: for p being XFinSequence for x being set st S1[p] holds S1[p ^ <%x%>] proof let p be XFinSequence; ::_thesis: for x being set st S1[p] holds S1[p ^ <%x%>] let x be set ; ::_thesis: ( S1[p] implies S1[p ^ <%x%>] ) assume A36: S1[p] ; ::_thesis: S1[p ^ <%x%>] let X be set ; ::_thesis: ( ex k being Nat st X c= k & p ^ <%x%> is XFinSequence of NAT & rng (p ^ <%x%>) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds k1 < k2 ) implies for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) holds q = p ^ <%x%> ) given k being Nat such that A37: X c= k ; ::_thesis: ( not p ^ <%x%> is XFinSequence of NAT or not rng (p ^ <%x%>) = X or ex l, m, k1, k2 being Nat st ( l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m & not k1 < k2 ) or for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) holds q = p ^ <%x%> ) assume that A38: p ^ <%x%> is XFinSequence of NAT and A39: rng (p ^ <%x%>) = X and A40: for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds k1 < k2 ; ::_thesis: for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) holds q = p ^ <%x%> let q be XFinSequence of NAT ; ::_thesis: ( rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ) implies q = p ^ <%x%> ) assume that A41: rng q = X and A42: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds k1 < k2 ; ::_thesis: q = p ^ <%x%> deffunc H1( Nat) -> Element of NAT = q . $1; len q <> 0 proof assume len q = 0 ; ::_thesis: contradiction then p ^ <%x%> = {} by A39, A41, AFINSQ_1:15, RELAT_1:38; then 0 = len (p ^ <%x%>) .= (len p) + (len <%x%>) by AFINSQ_1:17 .= 1 + (len p) by AFINSQ_1:34 ; hence contradiction ; ::_thesis: verum end; then consider n being Nat such that A43: len q = n + 1 by NAT_1:6; A44: ex m being Nat st ( m = x & ( for l being Nat st l in X & l <> x holds l < m ) ) proof <%x%> is XFinSequence of NAT by A38, AFINSQ_1:31; then rng <%x%> c= NAT by RELAT_1:def_19; then {x} c= NAT by AFINSQ_1:33; then reconsider m = x as Element of NAT by ZFMISC_1:31; take m ; ::_thesis: ( m = x & ( for l being Nat st l in X & l <> x holds l < m ) ) thus m = x ; ::_thesis: for l being Nat st l in X & l <> x holds l < m thus for l being Nat st l in X & l <> x holds l < m ::_thesis: verum proof len <%x%> = 1 by AFINSQ_1:34; then A45: m = (p ^ <%x%>) . (((len p) + (len <%x%>)) - 1) by AFINSQ_1:36 .= (p ^ <%x%>) . ((len (p ^ <%x%>)) - 1) by AFINSQ_1:17 ; len (p ^ <%x%>) < (len (p ^ <%x%>)) + 1 by XREAL_1:29; then A46: (len (p ^ <%x%>)) - 1 < len (p ^ <%x%>) by XREAL_1:19; let l be Nat; ::_thesis: ( l in X & l <> x implies l < m ) assume that A47: l in X and A48: l <> x ; ::_thesis: l < m consider y being set such that A49: y in dom (p ^ <%x%>) and A50: l = (p ^ <%x%>) . y by A39, A47, FUNCT_1:def_3; reconsider k = y as Element of NAT by A49; k < len (p ^ <%x%>) by A49, NAT_1:44; then k < (len p) + (len <%x%>) by AFINSQ_1:17; then k < (len p) + 1 by AFINSQ_1:34; then A51: k <= len p by NAT_1:13; k <> len p by A48, A50, AFINSQ_1:36; then k < ((len p) + 1) - 1 by A51, XXREAL_0:1; then k < ((len p) + (len <%x%>)) - 1 by AFINSQ_1:34; then A52: k < (len (p ^ <%x%>)) - 1 by AFINSQ_1:17; then (len (p ^ <%x%>)) -' 1 = (len (p ^ <%x%>)) - 1 by XREAL_0:def_2; hence l < m by A40, A50, A52, A46, A45; ::_thesis: verum end; end; then reconsider m = x as Nat ; A53: not x in rng p proof (len p) + 1 = (len p) + (len <%x%>) by AFINSQ_1:34 .= len (p ^ <%x%>) by AFINSQ_1:17 ; then A54: len p < len (p ^ <%x%>) by XREAL_1:29; A55: m = (p ^ <%x%>) . (len p) by AFINSQ_1:36; assume x in rng p ; ::_thesis: contradiction then consider y being set such that A56: y in dom p and A57: x = p . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A56; A58: y < len p by A56, NAT_1:44; m = (p ^ <%x%>) . y by A56, A57, AFINSQ_1:def_3; hence contradiction by A40, A58, A54, A55; ::_thesis: verum end; A59: for z being set holds ( z in ((rng p) \/ {x}) \ {x} iff z in rng p ) proof let z be set ; ::_thesis: ( z in ((rng p) \/ {x}) \ {x} iff z in rng p ) thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) ::_thesis: ( z in rng p implies z in ((rng p) \/ {x}) \ {x} ) proof assume A60: z in ((rng p) \/ {x}) \ {x} ; ::_thesis: z in rng p then not z in {x} by XBOOLE_0:def_5; hence z in rng p by A60, XBOOLE_0:def_3; ::_thesis: verum end; assume A61: z in rng p ; ::_thesis: z in ((rng p) \/ {x}) \ {x} then A62: z in (rng p) \/ {x} by XBOOLE_0:def_3; not z in {x} by A53, A61, TARSKI:def_1; hence z in ((rng p) \/ {x}) \ {x} by A62, XBOOLE_0:def_5; ::_thesis: verum end; deffunc H2( set ) -> Element of NAT = q . $1; consider q9 being XFinSequence such that A63: len q9 = n and A64: for m being Nat st m in n holds q9 . m = H2(m) from AFINSQ_1:sch_2(); now__::_thesis:_for_x_being_set_st_x_in_rng_q9_holds_ x_in_NAT let x be set ; ::_thesis: ( x in rng q9 implies x in NAT ) assume x in rng q9 ; ::_thesis: x in NAT then consider y being set such that A65: y in dom q9 and A66: x = q9 . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A65; q . y in NAT ; hence x in NAT by A63, A64, A65, A66; ::_thesis: verum end; then rng q9 c= NAT by TARSKI:def_3; then reconsider f = q9 as XFinSequence of NAT by RELAT_1:def_19; A67: p is XFinSequence of NAT by A38, AFINSQ_1:31; A68: for m being Nat st m in dom <%x%> holds q . ((len q9) + m) = <%x%> . m proof let m be Nat; ::_thesis: ( m in dom <%x%> implies q . ((len q9) + m) = <%x%> . m ) assume m in dom <%x%> ; ::_thesis: q . ((len q9) + m) = <%x%> . m then m in len <%x%> ; then A69: m in 1 by AFINSQ_1:34; 0 + 1 = 0 \/ {0} by AFINSQ_1:2; then A70: m = 0 by A69, TARSKI:def_1; q . ((len q9) + m) = x proof x in {x} by TARSKI:def_1; then x in rng <%x%> by AFINSQ_1:33; then x in (rng p) \/ (rng <%x%>) by XBOOLE_0:def_3; then x in rng q by A39, A41, AFINSQ_1:26; then consider y being set such that A71: y in dom q and A72: x = q . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A71; y < len q by A71, NAT_1:44; then y + 1 <= len q by NAT_1:13; then A73: y <= (len q) - 1 by XREAL_1:19; len q < (len q) + 1 by XREAL_1:29; then (len q) - 1 < len q by XREAL_1:19; then (len q) - 1 in dom q by A43, NAT_1:44; then A74: q . ((len q) - 1) in X by A41, FUNCT_1:def_3; len q < (len q) + 1 by XREAL_1:29; then A75: ( ( y < (len q) - 1 & (len q) - 1 < len q ) or y = (len q) - 1 ) by A73, XREAL_1:19, XXREAL_0:1; set k = q . ((len q) - 1); consider d being Nat such that A76: d = x and A77: for l being Nat st l in X & l <> x holds l < d by A44; assume q . ((len q9) + m) <> x ; ::_thesis: contradiction then q . ((len q) - 1) < d by A43, A63, A70, A77, A74; hence contradiction by A42, A43, A76, A72, A75; ::_thesis: verum end; hence q . ((len q9) + m) = <%x%> . m by A70, AFINSQ_1:34; ::_thesis: verum end; A78: dom q = (len q9) + (len <%x%>) by A43, A63, AFINSQ_1:34; then A79: q9 ^ <%x%> = q by A63, A64, A68, AFINSQ_1:def_3; A80: not x in rng f proof (len f) + 1 = (len f) + (len <%x%>) by AFINSQ_1:34 .= len (f ^ <%x%>) by AFINSQ_1:17 ; then A81: len f < len (f ^ <%x%>) by XREAL_1:29; A82: m = q . (len f) by A79, AFINSQ_1:36; assume x in rng f ; ::_thesis: contradiction then consider y being set such that A83: y in dom f and A84: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A83; A85: y < len f by A83, NAT_1:44; m = q . y by A63, A64, A83, A84; hence contradiction by A42, A79, A85, A81, A82; ::_thesis: verum end; A86: for z being set holds ( z in ((rng f) \/ {x}) \ {x} iff z in rng f ) proof let z be set ; ::_thesis: ( z in ((rng f) \/ {x}) \ {x} iff z in rng f ) thus ( z in ((rng f) \/ {x}) \ {x} implies z in rng f ) ::_thesis: ( z in rng f implies z in ((rng f) \/ {x}) \ {x} ) proof assume A87: z in ((rng f) \/ {x}) \ {x} ; ::_thesis: z in rng f then not z in {x} by XBOOLE_0:def_5; hence z in rng f by A87, XBOOLE_0:def_3; ::_thesis: verum end; assume A88: z in rng f ; ::_thesis: z in ((rng f) \/ {x}) \ {x} then A89: z in (rng f) \/ {x} by XBOOLE_0:def_3; not z in {x} by A80, A88, TARSKI:def_1; hence z in ((rng f) \/ {x}) \ {x} by A89, XBOOLE_0:def_5; ::_thesis: verum end; X = (rng p) \/ (rng <%x%>) by A39, AFINSQ_1:26 .= (rng p) \/ {x} by AFINSQ_1:33 ; then A90: rng p = X \ {x} by A59, TARSKI:1; A91: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds k1 < k2 proof let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len p & k1 = p . l & k2 = p . m implies k1 < k2 ) assume that A92: l < m and A93: m < len p and A94: k1 = p . l and A95: k2 = p . m ; ::_thesis: k1 < k2 l < len p by A92, A93, XXREAL_0:2; then l in dom p by NAT_1:44; then A96: k1 = (p ^ <%x%>) . l by A94, AFINSQ_1:def_3; len p < (len p) + 1 by XREAL_1:29; then m < (len p) + 1 by A93, XXREAL_0:2; then m < (len p) + (len <%x%>) by AFINSQ_1:34; then A97: m < len (p ^ <%x%>) by AFINSQ_1:17; m in dom p by A93, NAT_1:44; then k2 = (p ^ <%x%>) . m by A95, AFINSQ_1:def_3; hence k1 < k2 by A40, A92, A96, A97; ::_thesis: verum end; A98: for l, m, k1, k2 being Nat st l < m & m < len f & k1 = f . l & k2 = f . m holds k1 < k2 proof let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len f & k1 = f . l & k2 = f . m implies k1 < k2 ) assume that A99: l < m and A100: m < len f and A101: k1 = f . l and A102: k2 = f . m ; ::_thesis: k1 < k2 m in n by A63, A100, NAT_1:44; then A103: k2 = q . m by A64, A102; l < n by A63, A99, A100, XXREAL_0:2; then l in n by NAT_1:44; then A104: k1 = q . l by A64, A101; m < len q by A43, A63, A100, NAT_1:13; hence k1 < k2 by A42, A99, A104, A103; ::_thesis: verum end; X = (rng f) \/ (rng <%x%>) by A41, A79, AFINSQ_1:26 .= (rng f) \/ {x} by AFINSQ_1:33 ; then A105: rng f = X \ {x} by A86, TARSKI:1; ex m being Nat st X \ {x} c= m by A37, XBOOLE_1:1; then q9 = p by A36, A91, A67, A90, A98, A105; hence q = p ^ <%x%> by A63, A64, A78, A68, AFINSQ_1:def_3; ::_thesis: verum end; A106: S1[ {} ] ; A107: for p being XFinSequence holds S1[p] from AFINSQ_1:sch_3(A106, A35); ex k being Nat st X c= k by Th2; hence p = q by A31, A32, A33, A34, A107; ::_thesis: verum end; end; :: deftheorem Def4 defines Sgm0 AFINSQ_2:def_4_:_ for X being finite natural-membered set for b2 being XFinSequence of NAT holds ( b2 = Sgm0 X iff ( rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds k1 < k2 ) ) ); registration let A be finite natural-membered set ; cluster Sgm0 A -> one-to-one ; coherence Sgm0 A is one-to-one proof for x, y being set st x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y holds not x <> y proof let x, y be set ; ::_thesis: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y implies not x <> y ) assume that A1: x in dom (Sgm0 A) and A2: y in dom (Sgm0 A) and A3: (Sgm0 A) . x = (Sgm0 A) . y and A4: x <> y ; ::_thesis: contradiction reconsider i = x, j = y as Element of NAT by A1, A2; percases ( i < j or j < i ) by A4, XXREAL_0:1; supposeA5: i < j ; ::_thesis: contradiction j < len (Sgm0 A) by A2, NAT_1:44; hence contradiction by A3, A5, Def4; ::_thesis: verum end; supposeA6: j < i ; ::_thesis: contradiction i < len (Sgm0 A) by A1, NAT_1:44; hence contradiction by A3, A6, Def4; ::_thesis: verum end; end; end; hence Sgm0 A is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; end; theorem Th20: :: AFINSQ_2:20 for A being finite natural-membered set holds len (Sgm0 A) = card A proof let A be finite natural-membered set ; ::_thesis: len (Sgm0 A) = card A rng (Sgm0 A) = A by Def4; then len (Sgm0 A),A are_equipotent by WELLORD2:def_4; then card A = card (len (Sgm0 A)) by CARD_1:5; hence len (Sgm0 A) = card A ; ::_thesis: verum end; theorem Th21: :: AFINSQ_2:21 for X, Y being finite natural-membered set st X c= Y & X <> {} holds (Sgm0 Y) . 0 <= (Sgm0 X) . 0 proof let X, Y be finite natural-membered set ; ::_thesis: ( X c= Y & X <> {} implies (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ) assume that A1: X c= Y and A2: X <> {} ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0 reconsider X0 = X as finite set ; 0 <> card X0 by A2; then 0 < len (Sgm0 X) by Th20; then A3: 0 in dom (Sgm0 X) by NAT_1:44; A4: rng (Sgm0 Y) = Y by Def4; rng (Sgm0 X) = X by Def4; then (Sgm0 X) . 0 in X by A3, FUNCT_1:def_3; then consider x being set such that A5: x in dom (Sgm0 Y) and A6: (Sgm0 Y) . x = (Sgm0 X) . 0 by A1, A4, FUNCT_1:def_3; reconsider nx = x as Nat by A5; A7: nx < len (Sgm0 Y) by A5, NAT_1:44; now__::_thesis:_(_(_0_<>_nx_&_(Sgm0_Y)_._0_<=_(Sgm0_X)_._0_)_or_(_0_=_nx_&_(Sgm0_Y)_._0_<=_(Sgm0_X)_._0_)_) percases ( 0 <> nx or 0 = nx ) ; case 0 <> nx ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0 hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6, A7, Def4; ::_thesis: verum end; case 0 = nx ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0 hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6; ::_thesis: verum end; end; end; hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ; ::_thesis: verum end; theorem Th22: :: AFINSQ_2:22 for n being Nat holds (Sgm0 {n}) . 0 = n proof let n be Nat; ::_thesis: (Sgm0 {n}) . 0 = n len (Sgm0 {n}) = card {n} by Th20; then 0 in dom (Sgm0 {n}) by NAT_1:44; then A1: (Sgm0 {n}) . 0 in rng (Sgm0 {n}) by FUNCT_1:def_3; rng (Sgm0 {n}) = {n} by Def4; hence (Sgm0 {n}) . 0 = n by A1, TARSKI:def_1; ::_thesis: verum end; definition let B1, B2 be set ; predB1 _{} set x = the Element of (B1 /\ B2) /\ NAT; reconsider nx = the Element of (B1 /\ B2) /\ NAT as Nat ; assume (B1 /\ B2) /\ NAT <> {} ; ::_thesis: contradiction then A2: the Element of (B1 /\ B2) /\ NAT in B1 /\ B2 by XBOOLE_0:def_4; then A3: nx in B2 by XBOOLE_0:def_4; nx in B1 by A2, XBOOLE_0:def_4; hence contradiction by A1, A3, Def5; ::_thesis: verum end; hence (B1 /\ B2) /\ NAT = {} ; ::_thesis: verum end; theorem :: AFINSQ_2:24 for B1, B2 being finite natural-membered set st B1 {} by XBOOLE_0:def_7; then A3: the Element of B1 /\ B2 in B2 by XBOOLE_0:def_4; the Element of B1 /\ B2 in B1 by A2, XBOOLE_0:def_4; hence contradiction by A1, A3, Def5; ::_thesis: verum end; hence B1 misses B2 ; ::_thesis: verum end; theorem Th25: :: AFINSQ_2:25 for A, B1, B2 being set st B1 {} & ex x being set st ( x in X & {x} {} & ex x being set st ( x in X & {x} {} and A2: ex x being set st ( x in X & {x} card Y by A1; then 0 < len (Sgm0 Y) by Th20; then A5: 0 in dom (Sgm0 Y) by NAT_1:44; rng (Sgm0 Y) = Y by Def4; then A6: (Sgm0 Y) . 0 in Y by A5, FUNCT_1:def_3; reconsider x0 = x as Element of NAT by A3, ORDINAL1:def_12; set nx = x0; x0 in {x0} by TARSKI:def_1; then A7: x0 <= (Sgm0 Y) . 0 by A4, A6, Def6; {x0} c= X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in X ) assume y in {x0} ; ::_thesis: y in X hence y in X by A3, TARSKI:def_1; ::_thesis: verum end; then A8: (Sgm0 X) . 0 <= (Sgm0 {x0}) . 0 by Th21; (Sgm0 {x0}) . 0 = x0 by Th22; hence (Sgm0 X) . 0 <= (Sgm0 Y) . 0 by A8, A7, XXREAL_0:2; ::_thesis: verum end; theorem Th27: :: AFINSQ_2:27 for i being Nat for X0, Y0 being finite natural-membered set st X0 {} by A2, CARD_1:27, XBOOLE_1:15; A18: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X0_\/_Y0))_|_(card_X0))_._k2_&_k2_in_card_X0_)__}__c=_X0_implies_X0_c=__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X0_\/_Y0))_|_(card_X0))_._k2_&_k2_in_card_X0_)__}__) assume that A19: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } c= X0 and A20: not X0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } ; ::_thesis: contradiction consider v1 being set such that A21: v1 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } and A22: not v1 in X0 by A19, TARSKI:def_3; consider v10 being Element of X0 \/ Y0 such that A23: v1 = v10 and A24: ex k2 being Nat st ( v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) by A21; A25: v10 in Y0 by A17, A22, A23, XBOOLE_0:def_3; reconsider nv10 = v10 as Nat ; consider v2 being set such that A26: v2 in X0 and A27: not v2 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } by A20, TARSKI:def_3; X0 c= X0 \/ Y0 by XBOOLE_1:7; then consider x2 being set such that A28: x2 in dom (Sgm0 (X0 \/ Y0)) and A29: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A11, A26, FUNCT_1:def_3; reconsider x20 = x2 as Nat by A28; reconsider nv2 = v2 as Nat by A29; A30: x20 < len (Sgm0 (X0 \/ Y0)) by A28, NAT_1:44; A31: now__::_thesis:_not_x20_<_card_X0 assume x20 < card X0 ; ::_thesis: contradiction then A32: x20 in card X0 by NAT_1:44; card X0 <= card (X0 \/ Y0) by NAT_1:43, XBOOLE_1:7; then card X0 <= len (Sgm0 (X0 \/ Y0)) by Th20; then ((Sgm0 (X0 \/ Y0)) | (card X0)) . x20 = (Sgm0 (X0 \/ Y0)) . x20 by A32, AFINSQ_1:53; hence contradiction by A4, A26, A27, A29, A32; ::_thesis: verum end; consider k20 being Nat such that A33: v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 and A34: k20 in card X0 by A24; card X0 <= len (Sgm0 (X0 \/ Y0)) by A10, NAT_1:43, XBOOLE_1:7; then A35: ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . k20 by A34, AFINSQ_1:53; k20 < len ((Sgm0 (X0 \/ Y0)) | (card X0)) by A6, A34, NAT_1:44; then k20 < x20 by A6, A31, XXREAL_0:2; then nv10 < nv2 by A33, A29, A35, A30, Def4; hence contradiction by A1, A26, A25, Def5; ::_thesis: verum end; A36: now__::_thesis:_(_(_Z0_c=_X0_&_Z0_=_X0_)_or_(_X0_c=_Z0_&_Z0_=_X0_)_) percases ( Z0 c= X0 or X0 c= Z0 ) by A18; case Z0 c= X0 ; ::_thesis: Z0 = X0 hence Z0 = X0 by A16, Lm1; ::_thesis: verum end; case X0 c= Z0 ; ::_thesis: Z0 = X0 hence Z0 = X0 by A16, Lm1; ::_thesis: verum end; end; end; card X0 <= len (Sgm0 (X0 \/ Y0)) by A5, NAT_1:43, XBOOLE_1:7; hence ( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i ) by A12, A7, A36, A3, AFINSQ_1:53, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: AFINSQ_2:28 for i being Nat for X, Y being finite natural-membered set st X {} by A2, CARD_1:27, XBOOLE_1:15; A12: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X_\/_Y_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X_\/_Y))_|_(card_X))_._k2_&_k2_in_card_X_)__}__c=_X_implies_X_c=__{__v_where_v_is_Element_of_X_\/_Y_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X_\/_Y))_|_(card_X))_._k2_&_k2_in_card_X_)__}__) assume that A13: not { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= X and A14: not X c= { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; ::_thesis: contradiction consider v1 being set such that A15: v1 in { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } and A16: not v1 in X by A13, TARSKI:def_3; consider v10 being Element of X \/ Y such that A17: v1 = v10 and A18: ex k2 being Nat st ( v10 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) by A15; A19: v10 in Y by A11, A16, A17, XBOOLE_0:def_3; reconsider nv10 = v10 as Nat ; consider v2 being set such that A20: v2 in X and A21: not v2 in { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } by A14, TARSKI:def_3; X c= X \/ Y by XBOOLE_1:7; then consider x2 being set such that A22: x2 in dom (Sgm0 (X \/ Y)) and A23: v2 = (Sgm0 (X \/ Y)) . x2 by A3, A20, FUNCT_1:def_3; reconsider x20 = x2 as Nat by A22; now__::_thesis:_not_x20_<_card_X assume x20 < card X ; ::_thesis: contradiction then A24: x20 in card X by NAT_1:44; card X <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7; then card X <= len (Sgm0 (X \/ Y)) by Th20; then ((Sgm0 (X \/ Y)) | (card X)) . x20 = (Sgm0 (X \/ Y)) . x20 by A24, AFINSQ_1:53; hence contradiction by A5, A10, A21, A23, A24, FUNCT_1:def_3; ::_thesis: verum end; then A25: len ((Sgm0 (X \/ Y)) | (card X)) <= x20 by A4, AFINSQ_1:54; consider k20 being Nat such that A26: v10 = ((Sgm0 (X \/ Y)) | (card X)) . k20 and A27: k20 in card X by A18; A28: ((Sgm0 (X \/ Y)) | (card X)) . k20 = (Sgm0 (X \/ Y)) . k20 by A4, A27, AFINSQ_1:53; reconsider nv2 = v2 as Nat by A23; k20 < len ((Sgm0 (X \/ Y)) | (card X)) by A5, A27, NAT_1:44; then A29: k20 < x20 by A25, XXREAL_0:2; x20 < len (Sgm0 (X \/ Y)) by A22, NAT_1:44; then nv10 < nv2 by A26, A23, A29, A28, Def4; hence contradiction by A1, A20, A19, Def5; ::_thesis: verum end; (Sgm0 (X \/ Y)) | (card X) is one-to-one by FUNCT_1:52; then A30: dom ((Sgm0 (X \/ Y)) | (card X)),((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) are_equipotent by CARD_1:33; ((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) = rng ((Sgm0 (X \/ Y)) | (card X)) by RELAT_1:113; then A31: card { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card (len ((Sgm0 (X \/ Y)) | (card X))) by A10, A30, CARD_1:5; then A32: card { v where v is Element of X \/ Y : ex k2 being Nat st ( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card X by A4, AFINSQ_1:54; A33: now__::_thesis:_(_(_Z0_c=_X_&_Z0_=_X_)_or_(_X_c=_Z0_&_Z0_=_X_)_) percases ( Z0 c= X or X c= Z0 ) by A12; case Z0 c= X ; ::_thesis: Z0 = X hence Z0 = X by A4, A31, Lm1, AFINSQ_1:54; ::_thesis: verum end; case X c= Z0 ; ::_thesis: Z0 = X hence Z0 = X by A32, Lm1; ::_thesis: verum end; end; end; ((Sgm0 (X \/ Y)) | (card X)) . i = (Sgm0 (X \/ Y)) . i by A2, A4, AFINSQ_1:53; hence (Sgm0 (X \/ Y)) . i in X by A2, A5, A10, A33, FUNCT_1:def_3; ::_thesis: verum end; theorem Th29: :: AFINSQ_2:29 for i being Nat for X, Y being finite natural-membered set st X {} by A2, CARD_1:27, XBOOLE_1:15; A22: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X0_\/_Y0))_/^_(card_X0))_._k2_&_k2_in_card_Y0_)__}__c=_Y0_implies_Y0_c=__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_ (_v_=_((Sgm0_(X0_\/_Y0))_/^_(card_X0))_._k2_&_k2_in_card_Y0_)__}__) assume that A23: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= Y0 and A24: not Y0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ; ::_thesis: contradiction consider v2 being set such that A25: v2 in Y0 and A26: not v2 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } by A24, TARSKI:def_3; Y0 c= X0 \/ Y0 by XBOOLE_1:7; then consider x2 being set such that A27: x2 in dom (Sgm0 (X0 \/ Y0)) and A28: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A6, A25, FUNCT_1:def_3; consider v1 being set such that A29: v1 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st ( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } and A30: not v1 in Y0 by A23, TARSKI:def_3; consider v10 being Element of X0 \/ Y0 such that A31: v1 = v10 and A32: ex k2 being Nat st ( v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) by A29; A33: v10 in X0 by A21, A30, A31, XBOOLE_0:def_3; reconsider nv10 = v10 as Nat ; reconsider nv2 = v2 as Nat by A28; consider k20 being Nat such that A34: v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 and A35: k20 in card Y0 by A32; k20 < card Y0 by A35, NAT_1:44; then A36: k20 + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, XREAL_1:6; then A37: ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . (k20 + (card X0)) by Th8; reconsider x20 = x2 as Nat by A27; set nx20 = x20 -' (card X0); A38: v2 in X0 \/ Y0 by A6, A27, A28, FUNCT_1:def_3; A39: now__::_thesis:_not_x20_>=_card_X0 assume A40: x20 >= card X0 ; ::_thesis: contradiction then A41: x20 -' (card X0) = x20 - (card X0) by XREAL_1:233; x20 < (card X0) + (card Y0) by A20, A27, NAT_1:44; then x20 - (card X0) < ((card X0) + (card Y0)) - (card X0) by XREAL_1:9; then A42: x20 -' (card X0) < card Y0 by A40, XREAL_1:233; then A43: x20 -' (card X0) in card Y0 by NAT_1:44; (x20 -' (card X0)) + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, A42, XREAL_1:6; then ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . (x20 -' (card X0)) = (Sgm0 (X0 \/ Y0)) . x20 by A41, Th8; hence contradiction by A26, A28, A38, A43; ::_thesis: verum end; card X0 <= (card X0) + k20 by NAT_1:12; then k20 + (card X0) > x20 by A39, XXREAL_0:2; then nv10 > nv2 by A34, A28, A36, A37, Def4; hence contradiction by A1, A25, A33, Def5; ::_thesis: verum end; A44: now__::_thesis:_(_(_Z0_c=_Y0_&_Z0_=_Y0_)_or_(_Y0_c=_Z0_&_Z0_=_Y0_)_) percases ( Z0 c= Y0 or Y0 c= Z0 ) by A22; case Z0 c= Y0 ; ::_thesis: Z0 = Y0 hence Z0 = Y0 by A19, Lm1; ::_thesis: verum end; case Y0 c= Z0 ; ::_thesis: Z0 = Y0 hence Z0 = Y0 by A19, Lm1; ::_thesis: verum end; end; end; i + (card X0) < len (Sgm0 (X0 \/ Y0)) by A2, A9, A11, XREAL_1:20; hence ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) by A15, A12, A44, Th8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th31: :: AFINSQ_2:31 for i being Nat for X, Y being finite natural-membered set st X {} & X {} & X {} and A2: X 0 by A1; then 0 < len (Sgm0 Y) by Th20; then (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (0 + (len (Sgm0 X))) by A2, Th31; hence (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X)) ; ::_thesis: verum end; theorem Th33: :: AFINSQ_2:33 for l, m, n, k being Nat for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds m < n proof let l, m, n, k be Nat; ::_thesis: for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds m < n let X be finite natural-membered set ; ::_thesis: ( k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l implies m < n ) assume that A1: k < l and A2: m < len (Sgm0 X) and A3: (Sgm0 X) . m = k and A4: (Sgm0 X) . n = l and A5: not m < n ; ::_thesis: contradiction n < m by A1, A3, A4, A5, XXREAL_0:1; hence contradiction by A1, A2, A3, A4, Def4; ::_thesis: verum end; theorem Th34: :: AFINSQ_2:34 for X, Y being finite natural-membered set st X <> {} & X {} & X {} and A2: X 0 by A1; then 0 < len (Sgm0 X) by Th20; hence (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 by A2, Th29; ::_thesis: verum end; theorem Th35: :: AFINSQ_2:35 for X, Y being finite natural-membered set holds ( X (Sgm0 X) . (k + 1) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( k in dom (Sgm0 X) or not k in dom (Sgm0 X) ) ; supposeA14: k in dom (Sgm0 X) ; ::_thesis: contradiction set m1 = (Sgm0 (X \/ Y)) . k; set n1 = (Sgm0 X) . k; now__::_thesis:_contradiction percases ( (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) or (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ) by A13, XXREAL_0:1; supposeA15: (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) ; ::_thesis: contradiction then not (Sgm0 (X \/ Y)) . (k + 1) in Y by A1, A10, Def5; then (Sgm0 (X \/ Y)) . (k + 1) in X by A12, XBOOLE_0:def_3; then (Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 X) by Def4; then consider x being set such that A16: x in dom (Sgm0 X) and A17: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . (k + 1) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A16; x < len (Sgm0 X) by A16, NAT_1:44; then A18: x < k + 1 by A15, A17, Th33; A19: k < k + 1 by XREAL_1:29; k + 1 < len (Sgm0 (X \/ Y)) by A9, A11, NAT_1:44; then A20: (Sgm0 X) . k < (Sgm0 (X \/ Y)) . (k + 1) by A8, A14, A19, Def4; k < len (Sgm0 X) by A14, NAT_1:44; then k < x by A17, A20, Th33; hence contradiction by A18, NAT_1:13; ::_thesis: verum end; supposeA21: (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ; ::_thesis: contradiction (Sgm0 X) . (k + 1) in X \/ Y by A10, XBOOLE_0:def_3; then (Sgm0 X) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4; then consider x being set such that A22: x in dom (Sgm0 (X \/ Y)) and A23: (Sgm0 (X \/ Y)) . x = (Sgm0 X) . (k + 1) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A22; x < len (Sgm0 (X \/ Y)) by A22, NAT_1:44; then A24: x < k + 1 by A21, A23, Th33; A25: k < k + 1 by XREAL_1:29; k + 1 < len (Sgm0 X) by A9, NAT_1:44; then A26: (Sgm0 (X \/ Y)) . k < (Sgm0 X) . (k + 1) by A8, A14, A25, Def4; k < len (Sgm0 (X \/ Y)) by A11, A14, NAT_1:44; then k < x by A23, A26, Th33; hence contradiction by A24, NAT_1:13; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA27: not k in dom (Sgm0 X) ; ::_thesis: contradiction A28: k < k + 1 by XREAL_1:29; len (Sgm0 X) <= k by A27, NAT_1:44; then len (Sgm0 X) < k + 1 by A28, XXREAL_0:2; hence contradiction by A9, NAT_1:44; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; ( 0 < len (Sgm0 X) implies X1 <> {} ) by Th20, CARD_1:27; then A29: S1[ 0 ] by A1, Th34; A30: for k being Nat holds S1[k] from NAT_1:sch_2(A29, A7); defpred S2[ Nat] means ( $1 in dom (Sgm0 Y) implies (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + $1) = (Sgm0 Y) . $1 ); A31: now__::_thesis:_for_k_being_Nat_st_S2[k]_holds_ S2[k_+_1] let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A32: S2[k] ; ::_thesis: S2[k + 1] thus S2[k + 1] ::_thesis: verum proof set n = (Sgm0 Y) . (k + 1); set a = (len (Sgm0 X)) + (k + 1); set m = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)); assume A33: k + 1 in dom (Sgm0 Y) ; ::_thesis: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) = (Sgm0 Y) . (k + 1) then (Sgm0 Y) . (k + 1) in rng (Sgm0 Y) by FUNCT_1:def_3; then A34: (Sgm0 Y) . (k + 1) in Y by Def4; k + 1 < len (Sgm0 Y) by A33, NAT_1:44; then A35: (len (Sgm0 X)) + (k + 1) < len (Sgm0 (X \/ Y)) by A6, XREAL_1:6; then A36: (len (Sgm0 X)) + (k + 1) in dom (Sgm0 (X \/ Y)) by NAT_1:44; then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 (X \/ Y)) by FUNCT_1:def_3; then A37: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X \/ Y by Def4; A38: now__::_thesis:_not_(Sgm0_(X_\/_Y))_._((len_(Sgm0_X))_+_(k_+_1))_in_X A39: len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by A6, NAT_1:12; assume (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X ; ::_thesis: contradiction then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 X) by Def4; then consider x being set such that A40: x in dom (Sgm0 X) and A41: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A40; x < len (Sgm0 X) by A40, NAT_1:44; then x < len (Sgm0 (X \/ Y)) by A39, XXREAL_0:2; then A42: x in dom (Sgm0 (X \/ Y)) by NAT_1:44; (Sgm0 (X \/ Y)) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A30, A40, A41; then x = (len (Sgm0 X)) + (k + 1) by A36, A42, FUNCT_1:def_4; then (len (Sgm0 X)) + (k + 1) <= (len (Sgm0 X)) + 0 by A40, NAT_1:44; hence contradiction by XREAL_1:29; ::_thesis: verum end; assume A43: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) <> (Sgm0 Y) . (k + 1) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( k in dom (Sgm0 Y) or not k in dom (Sgm0 Y) ) ; supposeA44: k in dom (Sgm0 Y) ; ::_thesis: contradiction set m1 = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k); set n1 = (Sgm0 Y) . k; A45: k < len (Sgm0 Y) by A44, NAT_1:44; now__::_thesis:_contradiction percases ( (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) or (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ) by A43, XXREAL_0:1; supposeA46: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) ; ::_thesis: contradiction (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in Y by A37, A38, XBOOLE_0:def_3; then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 Y) by Def4; then consider x being set such that A47: x in dom (Sgm0 Y) and A48: (Sgm0 Y) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A47; x < len (Sgm0 Y) by A47, NAT_1:44; then A49: x < k + 1 by A46, A48, Th33; (len (Sgm0 X)) + k < ((len (Sgm0 X)) + k) + 1 by XREAL_1:29; then A50: (Sgm0 Y) . k < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A32, A35, A44, Def4; k < len (Sgm0 Y) by A44, NAT_1:44; then k < x by A48, A50, Th33; hence contradiction by A49, NAT_1:13; ::_thesis: verum end; supposeA51: (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ; ::_thesis: contradiction (Sgm0 Y) . (k + 1) in X \/ Y by A34, XBOOLE_0:def_3; then (Sgm0 Y) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4; then consider x being set such that A52: x in dom (Sgm0 (X \/ Y)) and A53: (Sgm0 (X \/ Y)) . x = (Sgm0 Y) . (k + 1) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A52; x < len (Sgm0 (X \/ Y)) by A52, NAT_1:44; then A54: x < ((len (Sgm0 X)) + k) + 1 by A51, A53, Th33; A55: k < k + 1 by XREAL_1:29; k + 1 < len (Sgm0 Y) by A33, NAT_1:44; then A56: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k) < (Sgm0 Y) . (k + 1) by A32, A44, A55, Def4; (len (Sgm0 X)) + k < len (Sgm0 (X \/ Y)) by A6, A45, XREAL_1:6; then (len (Sgm0 X)) + k < x by A53, A56, Th33; hence contradiction by A54, NAT_1:13; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA57: not k in dom (Sgm0 Y) ; ::_thesis: contradiction A58: k < k + 1 by XREAL_1:29; len (Sgm0 Y) <= k by A57, NAT_1:44; then len (Sgm0 Y) < k + 1 by A58, XXREAL_0:2; hence contradiction by A33, NAT_1:44; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; ( len (Sgm0 Y) > 0 implies Y <> {} ) by Th20, CARD_1:27; then A59: S2[ 0 ] by A1, Th32; for k being Nat holds S2[k] from NAT_1:sch_2(A59, A31); hence Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) by A6, A30, AFINSQ_1:def_3; ::_thesis: verum end; assume A60: Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) ; ::_thesis: X XFinSequence equals :: AFINSQ_2:def 7 f * (Sgm0 (B /\ (len f))); coherence f * (Sgm0 (B /\ (len f))) is XFinSequence proof B /\ (len f) c= dom f by XBOOLE_1:17; then rng (Sgm0 (B /\ (len f))) c= dom f by Def4; hence f * (Sgm0 (B /\ (len f))) is XFinSequence by AFINSQ_1:10; ::_thesis: verum end; end; :: deftheorem defines SubXFinS AFINSQ_2:def_7_:_ for f being XFinSequence for B being set holds SubXFinS (f,B) = f * (Sgm0 (B /\ (len f))); theorem Th36: :: AFINSQ_2:36 for p being XFinSequence for B being set holds ( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) ) proof let p be XFinSequence; ::_thesis: for B being set holds ( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) ) let B be set ; ::_thesis: ( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) ) B /\ (len p) c= dom p by XBOOLE_1:17; then rng (Sgm0 (B /\ (len p))) c= dom p by Def4; then dom (SubXFinS (p,B)) = len (Sgm0 (B /\ (len p))) by RELAT_1:27 .= card (B /\ (len p)) by Th20 ; hence len (SubXFinS (p,B)) = card (B /\ (len p)) ; ::_thesis: for i being Nat st i < len (SubXFinS (p,B)) holds (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) let i be Nat; ::_thesis: ( i < len (SubXFinS (p,B)) implies (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) assume i < len (SubXFinS (p,B)) ; ::_thesis: (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) then i in dom (SubXFinS (p,B)) by NAT_1:44; hence (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) by FUNCT_1:12; ::_thesis: verum end; registration let D be set ; let f be XFinSequence of D; let B be set ; cluster SubXFinS (f,B) -> D -valued ; coherence SubXFinS (f,B) is D -valued ; end; registration let p be XFinSequence; cluster SubXFinS (p,{}) -> empty ; coherence SubXFinS (p,{}) is empty proof len (SubXFinS (p,{})) = card {} by Th36; hence SubXFinS (p,{}) is empty ; ::_thesis: verum end; end; registration let B be set ; cluster SubXFinS ({},B) -> empty ; coherence SubXFinS ({},B) is empty ; end; registration let n be Nat; let x be set ; clustern --> x -> T-Sequence-like ; coherence n --> x is T-Sequence-like ; end; scheme :: AFINSQ_2:sch 2 Sch5{ F1() -> set , P1[ set ] } : for F being XFinSequence of F1() holds P1[F] provided A1: P1[ <%> F1()] and A2: for F being XFinSequence of F1() for d being Element of F1() st P1[F] holds P1[F ^ <%d%>] proof defpred S1[ set ] means for F being XFinSequence of F1() st len F = $1 holds P1[F]; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: for F being XFinSequence of F1() st len F = n holds P1[F] ; ::_thesis: S1[n + 1] let F be XFinSequence of F1(); ::_thesis: ( len F = n + 1 implies P1[F] ) assume A5: len F = n + 1 ; ::_thesis: P1[F] then F <> {} ; then consider G being XFinSequence, d being set such that A6: F = G ^ <%d%> by AFINSQ_1:40; reconsider G = G, dd = <%d%> as XFinSequence of F1() by A6, AFINSQ_1:31; A7: ( rng dd c= F1() & rng dd = {d} & d in {d} ) by AFINSQ_1:33, TARSKI:def_1; len dd = 1 by AFINSQ_1:34; then len F = (len G) + 1 by A6, AFINSQ_1:17; hence P1[F] by A2, A4, A5, A6, A7; ::_thesis: verum end; let F be XFinSequence of F1(); ::_thesis: P1[F] A8: len F = len F ; for X being set st card X = {} holds X = {} ; then A9: S1[ 0 ] by A1; for n being Nat holds S1[n] from NAT_1:sch_2(A9, A3); hence P1[F] by A8; ::_thesis: verum end; definition let D be non empty set ; let F be XFinSequence; assume A1: F is D -valued ; let b be BinOp of D; assume A2: ( b is having_a_unity or len F >= 1 ) ; funcb "**" F -> Element of D means :Def8: :: AFINSQ_2:def 8 it = the_unity_wrt b if ( b is having_a_unity & len F = 0 ) otherwise ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & it = f . ((len F) - 1) ); existence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) proof now__::_thesis:_(_(_b_is_having_a_unity_&_len_F_=_0_implies_ex_b1_being_Element_of_D_st_b1_=_the_unity_wrt_b_)_&_(_(_not_b_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_._0_=_F_._0_&_(_for_n_being_Nat_st_n_+_1_<_len_F_holds_ f_._(n_+_1)_=_b_._((f_._n),(F_._(n_+_1)))_)_&_b1_=_f_._((len_F)_-_1)_)_)_) percases ( len F = 0 or len F <> 0 ) ; suppose len F = 0 ; ::_thesis: ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) by A2; ::_thesis: verum end; supposeA3: len F <> 0 ; ::_thesis: ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) defpred S1[ Nat] means for F being XFinSequence 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ); A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] let F be XFinSequence 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) ) assume that A6: len F = k + 1 and len F <> 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) set G = F | k; A7: k < k + 1 by NAT_1:13; then A8: len (F | k) = k by A6, AFINSQ_1:11; now__::_thesis:_ex_d_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_ (_f_._0_=_F_._0_&_(_for_n_being_Nat_st_n_+_1_<_len_F_holds_ f_._(n_+_1)_=_b_._((f_._n),(F_._(n_+_1)))_)_&_d_=_f_._((len_F)_-_1)_) percases ( len (F | k) = 0 or len (F | k) <> 0 ) ; supposeA9: len (F | k) = 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) then 0 in dom F by A6, A8, CARD_1:49, TARSKI:def_1; then A10: F . 0 in rng F by FUNCT_1:def_3; reconsider f = NAT --> (F . 0) as Function of NAT,D by A10, FUNCOP_1:45; take d = f . 0; ::_thesis: ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) take f = f; ::_thesis: ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) thus f . 0 = F . 0 by FUNCOP_1:7; ::_thesis: ( ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) thus for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) by A6, A8, A9, NAT_1:14; ::_thesis: d = f . ((len F) - 1) k < k + 1 by NAT_1:13; hence d = f . ((len F) - 1) by A6, A9, AFINSQ_1:11; ::_thesis: verum end; supposeA11: len (F | k) <> 0 ; ::_thesis: ex a being Element of D ex h being Function of NAT,D st ( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) ) k < len F by A6, NAT_1:13; then k in dom F by NAT_1:44; then A12: F . k in rng F by FUNCT_1:def_3; reconsider d1 = F . k as Element of D by A12; A13: 0 in len (F | k) by A11, NAT_1:44; consider d being Element of D, f being Function of NAT,D such that A14: f . 0 = (F | k) . 0 and A15: for n being Nat st n + 1 < len (F | k) holds f . (n + 1) = b . ((f . n),((F | k) . (n + 1))) and A16: d = f . ((len (F | k)) - 1) by A5, A6, A7, A11, AFINSQ_1:11; deffunc H1( Element of NAT ) -> Element of D = f . $1; reconsider K = k as Element of NAT by ORDINAL1:def_12; consider h being Function of NAT,D such that A17: h . K = b . (d,d1) and A18: for n being Element of NAT st n <> K holds h . n = H1(n) from FUNCT_2:sch_6(); take a = h . k; ::_thesis: ex h being Function of NAT,D st ( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) ) take h = h; ::_thesis: ( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) ) h . 0 = f . 0 by A8, A11, A18; hence h . 0 = F . 0 by A14, A13, FUNCT_1:47; ::_thesis: ( ( for n being Nat st n + 1 < len F holds h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) ) thus for n being Nat st n + 1 < len F holds h . (n + 1) = b . ((h . n),(F . (n + 1))) ::_thesis: a = h . ((len F) - 1) proof let n be Nat; ::_thesis: ( n + 1 < len F implies h . (n + 1) = b . ((h . n),(F . (n + 1))) ) assume n + 1 < len F ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1))) then A19: n + 1 <= len (F | k) by A6, A8, NAT_1:13; now__::_thesis:_h_._(n_+_1)_=_b_._((h_._n),(F_._(n_+_1))) percases ( n + 1 = len (F | k) or n + 1 < len (F | k) ) by A19, XXREAL_0:1; supposeA20: n + 1 = len (F | k) ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1))) then A21: n < k by A8, NAT_1:13; ( n + 1 = k & n in NAT ) by A6, A7, A20, AFINSQ_1:11, ORDINAL1:def_12; hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A16, A17, A18, A20, A21; ::_thesis: verum end; supposeA22: n + 1 < len (F | k) ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1))) then n + 1 in dom (F | k) by NAT_1:44; then A23: (F | k) . (n + 1) = F . (n + 1) by FUNCT_1:47; ( n <= n + 1 & n in NAT ) by NAT_1:11, ORDINAL1:def_12; then A24: f . n = h . n by A8, A18, A22; f . (n + 1) = h . (n + 1) by A8, A18, A22; hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A15, A22, A23, A24; ::_thesis: verum end; end; end; hence h . (n + 1) = b . ((h . n),(F . (n + 1))) ; ::_thesis: verum end; thus a = h . ((len F) - 1) by A6; ::_thesis: verum end; end; end; hence ex d being Element of D ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) ; ::_thesis: verum end; A25: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A25, A4); hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) by A1, A3; ::_thesis: verum end; end; end; hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of D holds ( ( b is having_a_unity & len F = 0 & b1 = the_unity_wrt b & b2 = the_unity_wrt b implies b1 = b2 ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b2 = f . ((len F) - 1) ) implies b1 = b2 ) ) proof let d1, d2 be Element of D; ::_thesis: ( ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 ) ) thus ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) ; ::_thesis: ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 ) A26: ((len F) - 1) + 1 = len F ; assume ( not b is having_a_unity or len F <> 0 ) ; ::_thesis: ( for f being Function of NAT,D holds ( not f . 0 = F . 0 or ex n being Nat st ( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d1 = f . ((len F) - 1) ) or for f being Function of NAT,D holds ( not f . 0 = F . 0 or ex n being Nat st ( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 ) then 0 < len F by A2; then A27: (len F) - 1 is Element of NAT by NAT_1:20; given f1 being Function of NAT,D such that A28: f1 . 0 = F . 0 and A29: for n being Nat st n + 1 < len F holds f1 . (n + 1) = b . ((f1 . n),(F . (n + 1))) and A30: d1 = f1 . ((len F) - 1) ; ::_thesis: ( for f being Function of NAT,D holds ( not f . 0 = F . 0 or ex n being Nat st ( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 ) given f2 being Function of NAT,D such that A31: f2 . 0 = F . 0 and A32: for n being Nat st n + 1 < len F holds f2 . (n + 1) = b . ((f2 . n),(F . (n + 1))) and A33: d2 = f2 . ((len F) - 1) ; ::_thesis: d1 = d2 defpred S1[ Nat] means ( $1 + 1 <= len F implies f1 . $1 = f2 . $1 ); A34: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A35: S1[n] ; ::_thesis: S1[n + 1] assume (n + 1) + 1 <= len F ; ::_thesis: f1 . (n + 1) = f2 . (n + 1) then A36: n + 1 < len F by NAT_1:13; then f2 . (n + 1) = b . ((f2 . n),(F . (n + 1))) by A32; hence f1 . (n + 1) = f2 . (n + 1) by A29, A35, A36; ::_thesis: verum end; A37: S1[ 0 ] by A28, A31; for n being Nat holds S1[n] from NAT_1:sch_2(A37, A34); hence d1 = d2 by A30, A33, A26, A27; ::_thesis: verum end; consistency for b1 being Element of D holds verum ; end; :: deftheorem Def8 defines "**" AFINSQ_2:def_8_:_ for D being non empty set for F being XFinSequence st F is D -valued holds for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds for b4 being Element of D holds ( ( b is having_a_unity & len F = 0 implies ( b4 = b "**" F iff b4 = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b4 = b "**" F iff ex f being Function of NAT,D st ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b4 = f . ((len F) - 1) ) ) ) ); theorem Th37: :: AFINSQ_2:37 for D being non empty set for b being BinOp of D for d being Element of D holds b "**" <%d%> = d proof let D be non empty set ; ::_thesis: for b being BinOp of D for d being Element of D holds b "**" <%d%> = d let b be BinOp of D; ::_thesis: for d being Element of D holds b "**" <%d%> = d let d be Element of D; ::_thesis: b "**" <%d%> = d len <%d%> = 1 by AFINSQ_1:33; then ex f being Function of NAT,D st ( f . 0 = <%d%> . 0 & ( for n being Nat st n + 1 < len <%d%> holds f . (n + 1) = b . ((f . n),(<%d%> . (n + 1))) ) & b "**" <%d%> = f . (1 - 1) ) by Def8; hence b "**" <%d%> = d by AFINSQ_1:34; ::_thesis: verum end; theorem Th38: :: AFINSQ_2:38 for D being non empty set for b being BinOp of D for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2) proof let D be non empty set ; ::_thesis: for b being BinOp of D for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2) let b be BinOp of D; ::_thesis: for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2) let d1, d2 be Element of D; ::_thesis: b "**" <%d1,d2%> = b . (d1,d2) A1: <%d1,d2%> . 0 = d1 by AFINSQ_1:38; len <%d1,d2%> = 2 by AFINSQ_1:38; then consider f being Function of NAT,D such that A2: f . 0 = <%d1,d2%> . 0 and A3: for n being Nat st n + 1 < 2 holds f . (n + 1) = b . ((f . n),(<%d1,d2%> . (n + 1))) and A4: b "**" <%d1,d2%> = f . (2 - 1) by Def8; f . (0 + 1) = b . ((f . 0),(<%d1,d2%> . (0 + 1))) by A3; hence b "**" <%d1,d2%> = b . (d1,d2) by A2, A4, A1, AFINSQ_1:38; ::_thesis: verum end; theorem Th39: :: AFINSQ_2:39 for D being non empty set for b being BinOp of D for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) proof let D be non empty set ; ::_thesis: for b being BinOp of D for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) let b be BinOp of D; ::_thesis: for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) let d, d1, d2 be Element of D; ::_thesis: b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) set F = <%d,d1,d2%>; A1: <%d,d1,d2%> . 0 = d by AFINSQ_1:39; A2: <%d,d1,d2%> . 1 = d1 by AFINSQ_1:39; len <%d,d1,d2%> = 3 by AFINSQ_1:39; then consider f being Function of NAT,D such that A3: f . 0 = <%d,d1,d2%> . 0 and A4: for n being Nat st n + 1 < 3 holds f . (n + 1) = b . ((f . n),(<%d,d1,d2%> . (n + 1))) and A5: b "**" <%d,d1,d2%> = f . (3 - 1) by Def8; A6: f . (1 + 1) = b . ((f . 1),(<%d,d1,d2%> . (1 + 1))) by A4; f . (0 + 1) = b . ((f . 0),(<%d,d1,d2%> . (0 + 1))) by A4; hence b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) by A3, A5, A6, A1, A2, AFINSQ_1:39; ::_thesis: verum end; theorem Th40: :: AFINSQ_2:40 for D being non empty set for F being XFinSequence of D for b being BinOp of D for d being Element of D st ( b is having_a_unity or len F > 0 ) holds b "**" (F ^ <%d%>) = b . ((b "**" F),d) proof let D be non empty set ; ::_thesis: for F being XFinSequence of D for b being BinOp of D for d being Element of D st ( b is having_a_unity or len F > 0 ) holds b "**" (F ^ <%d%>) = b . ((b "**" F),d) let F be XFinSequence of D; ::_thesis: for b being BinOp of D for d being Element of D st ( b is having_a_unity or len F > 0 ) holds b "**" (F ^ <%d%>) = b . ((b "**" F),d) let b be BinOp of D; ::_thesis: for d being Element of D st ( b is having_a_unity or len F > 0 ) holds b "**" (F ^ <%d%>) = b . ((b "**" F),d) let d be Element of D; ::_thesis: ( ( b is having_a_unity or len F > 0 ) implies b "**" (F ^ <%d%>) = b . ((b "**" F),d) ) assume A1: ( b is having_a_unity or len F > 0 ) ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d) now__::_thesis:_b_"**"_(F_^_<%d%>)_=_b_._((b_"**"_F),d) percases ( len F < 0 + 1 or len F >= 1 ) ; supposeA2: len F < 0 + 1 ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d) then A3: F = {} by NAT_1:13; {} ^ <%d%> = <%d%> ; then A4: b "**" (F ^ <%d%>) = d by Th37, A3; len F = 0 by A2, NAT_1:13; then b "**" F = the_unity_wrt b by A1, Def8; hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A1, A2, A4, NAT_1:13, SETWISEO:15; ::_thesis: verum end; supposeA5: len F >= 1 ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d) set G = F ^ <%d%>; reconsider lenF1 = (len F) - 1 as Element of NAT by A5, NAT_1:21; A6: (F ^ <%d%>) . (len F) = d by AFINSQ_1:36; A7: len (F ^ <%d%>) = (len F) + (len <%d%>) by AFINSQ_1:17 .= (len F) + 1 by AFINSQ_1:33 ; then 1 <= len (F ^ <%d%>) by NAT_1:12; then consider f1 being Function of NAT,D such that A8: f1 . 0 = (F ^ <%d%>) . 0 and A9: for n being Nat st n + 1 < len (F ^ <%d%>) holds f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) and A10: b "**" (F ^ <%d%>) = f1 . ((len (F ^ <%d%>)) - 1) by Def8; consider f being Function of NAT,D such that A11: f . 0 = F . 0 and A12: for n being Nat st n + 1 < len F holds f . (n + 1) = b . ((f . n),(F . (n + 1))) and A13: b "**" F = f . ((len F) - 1) by A5, Def8; defpred S1[ Nat] means ( $1 + 1 < len (F ^ <%d%>) implies f . $1 = f1 . $1 ); A14: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A15: S1[n] ; ::_thesis: S1[n + 1] set n1 = n + 1; assume A16: (n + 1) + 1 < len (F ^ <%d%>) ; ::_thesis: f . (n + 1) = f1 . (n + 1) then n + 1 < len (F ^ <%d%>) by NAT_1:13; then A17: f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) by A9; A18: ((n + 1) + 1) + (- 1) < ((len F) + 1) + (- 1) by A7, A16, XREAL_1:8; then A19: n + 1 in len F by NAT_1:44; f . (n + 1) = b . ((f . n),(F . (n + 1))) by A12, A18; hence f . (n + 1) = f1 . (n + 1) by A15, A16, A17, A19, AFINSQ_1:def_3, NAT_1:13; ::_thesis: verum end; 0 in len F by A5, NAT_1:44; then A20: S1[ 0 ] by A11, A8, AFINSQ_1:def_3; A21: for n being Nat holds S1[n] from NAT_1:sch_2(A20, A14); A22: lenF1 + 1 < len (F ^ <%d%>) by A7, NAT_1:13; then b "**" (F ^ <%d%>) = b . ((f1 . lenF1),((F ^ <%d%>) . (lenF1 + 1))) by A7, A9, A10; hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A13, A21, A22, A6; ::_thesis: verum end; end; end; hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) ; ::_thesis: verum end; theorem Th41: :: AFINSQ_2:41 for D being non empty set for F, G being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) proof let D be non empty set ; ::_thesis: for F, G being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) defpred S1[ XFinSequence of D] means for F being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds b "**" (F ^ $1) = b . ((b "**" F),(b "**" $1)); A1: for G being XFinSequence of D for d being Element of D st S1[G] holds S1[G ^ <%d%>] proof let G be XFinSequence 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 XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) holds b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) implies b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ) assume that A3: b is associative and A4: ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) now__::_thesis:_b_"**"_(F_^_(G_^_<%d%>))_=_b_._((b_"**"_F),(b_"**"_(G_^_<%d%>))) percases ( len G <> 0 or len G = 0 ) ; supposeA5: len G <> 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) then ( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + 0 ) ) by A4, AFINSQ_1:17, XREAL_1:8; then b . ((b "**" (F ^ G)),d) = b "**" ((F ^ G) ^ <%d%>) by Th40; then A6: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" (F ^ G)),d) by AFINSQ_1:27; len G >= 1 by A5, NAT_1:14; then b "**" (F ^ (G ^ <%d%>)) = b . ((b . ((b "**" F),(b "**" G))),d) by A2, A3, A4, A6 .= b . ((b "**" F),(b . ((b "**" G),d))) by A3, BINOP_1:def_3 .= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A5, Th40 ; hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum end; suppose len G = 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) then A7: G = {} ; hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ ({} ^ <%d%>)) .= b "**" (F ^ <%d%>) .= b . ((b "**" F),d) by A4, Th40 .= b . ((b "**" F),(b "**" ({} ^ <%d%>))) by Th37 .= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A7 ; ::_thesis: verum end; end; end; hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum end; A8: S1[ <%> D] proof let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) holds b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) implies b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) ) assume that b is associative and A9: ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) ; ::_thesis: b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) thus b "**" (F ^ (<%> D)) = b "**" (F ^ {}) .= b . ((b "**" F),(the_unity_wrt b)) by A9, SETWISEO:15 .= b . ((b "**" F),(b "**" (<%> D))) by A9, Def8, CARD_1:27 ; ::_thesis: verum end; for G being XFinSequence of D holds S1[G] from AFINSQ_2:sch_2(A8, A1); hence ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) ; ::_thesis: verum end; theorem Th42: :: AFINSQ_2:42 for D being non empty set for F, G being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) proof let D be non empty set ; ::_thesis: for F, G being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) defpred S1[ XFinSequence of D] means for F being XFinSequence of D for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds b "**" (F ^ $1) = b . ((b "**" F),(b "**" $1)); A1: for G being XFinSequence of D for d being Element of D st S1[G] holds S1[G ^ <%d%>] proof let G be XFinSequence 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 XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) holds b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) implies b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ) assume that A3: b is associative and A4: ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) now__::_thesis:_b_"**"_(F_^_(G_^_<%d%>))_=_b_._((b_"**"_F),(b_"**"_(G_^_<%d%>))) percases ( len G <> 0 or len G = 0 ) ; supposeA5: len G <> 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) then ( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + 0 ) ) by A4, AFINSQ_1:17, XREAL_1:8; then b . ((b "**" (F ^ G)),d) = b "**" ((F ^ G) ^ <%d%>) by Th40; then A6: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" (F ^ G)),d) by AFINSQ_1:27; len G >= 1 by A5, NAT_1:14; then b "**" (F ^ (G ^ <%d%>)) = b . ((b . ((b "**" F),(b "**" G))),d) by A2, A3, A4, A6 .= b . ((b "**" F),(b . ((b "**" G),d))) by A3, BINOP_1:def_3 .= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A5, Th40 ; hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum end; suppose len G = 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) then A7: G = {} ; hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ ({} ^ <%d%>)) .= b "**" (F ^ <%d%>) .= b . ((b "**" F),d) by A4, Th40 .= b . ((b "**" F),(b "**" ({} ^ <%d%>))) by Th37 .= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A7 ; ::_thesis: verum end; end; end; hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum end; A8: S1[ <%> D] proof let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) holds b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) implies b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) ) assume that b is associative and A9: ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) ; ::_thesis: b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) thus b "**" (F ^ (<%> D)) = b "**" (F ^ {}) .= b . ((b "**" F),(the_unity_wrt b)) by A9, SETWISEO:15 .= b . ((b "**" F),(b "**" (<%> D))) by A9, Def8, CARD_1:27 ; ::_thesis: verum end; for G being XFinSequence of D holds S1[G] from AFINSQ_2:sch_2(A8, A1); hence ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) ; ::_thesis: verum end; theorem Th43: :: AFINSQ_2:43 for n being Nat for D being non empty set for F being XFinSequence of D for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) proof let n be Nat; ::_thesis: for D being non empty set for F being XFinSequence of D for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) let D be non empty set ; ::_thesis: for F being XFinSequence of D for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) let F be XFinSequence of D; ::_thesis: for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) let b be BinOp of D; ::_thesis: ( n in dom F & ( b is having_a_unity or n <> 0 ) implies b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) ) assume that A1: n in dom F and A2: ( b is having_a_unity or n <> 0 ) ; ::_thesis: b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) len F > n by A1, NAT_1:44; then A3: len (F | n) = n by AFINSQ_1:54; defpred S1[ Nat] means ( $1 in dom F & ( b is having_a_unity or len (F | $1) >= 1 ) implies b . ((b "**" (F | $1)),(F . $1)) = b "**" (F | ($1 + 1)) ); A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] set k1 = k + 1; set Fk1 = F | (k + 1); set Fk2 = F | ((k + 1) + 1); assume that A5: k + 1 in dom F and A6: ( b is having_a_unity or len (F | (k + 1)) >= 1 ) ; ::_thesis: b . ((b "**" (F | (k + 1))),(F . (k + 1))) = b "**" (F | ((k + 1) + 1)) A7: 0 in dom F by A5, NAT_1:44; 0 in k + 1 by NAT_1:44; then 0 in (dom F) /\ (k + 1) by A7, XBOOLE_0:def_4; then 0 in dom (F | (k + 1)) by RELAT_1:61; then A8: (F | (k + 1)) . 0 = F . 0 by FUNCT_1:47; A9: k < k + 1 by NAT_1:13; k + 1 < (k + 1) + 1 by NAT_1:13; then k + 1 in (k + 1) + 1 by NAT_1:44; then A10: k + 1 in (dom F) /\ ((k + 1) + 1) by A5, XBOOLE_0:def_4; A11: dom F = len F ; A12: k + 1 < dom F by A5, NAT_1:44; then A13: len (F | (k + 1)) = k + 1 by A11, AFINSQ_1:54; then consider f1 being Function of NAT,D such that A14: f1 . 0 = (F | (k + 1)) . 0 and A15: for n being Nat st n + 1 < len (F | (k + 1)) holds f1 . (n + 1) = b . ((f1 . n),((F | (k + 1)) . (n + 1))) and A16: b "**" (F | (k + 1)) = f1 . ((k + 1) - 1) by A6, Def8; (k + 1) + 1 <= dom F by A12, NAT_1:13; then A17: len (F | ((k + 1) + 1)) = (k + 1) + 1 by A11, AFINSQ_1:54; then ( b is having_a_unity or len (F | ((k + 1) + 1)) >= 1 ) by A6, A13, NAT_1:13; then consider f2 being Function of NAT,D such that A18: f2 . 0 = (F | ((k + 1) + 1)) . 0 and A19: for n being Nat st n + 1 < len (F | ((k + 1) + 1)) holds f2 . (n + 1) = b . ((f2 . n),((F | ((k + 1) + 1)) . (n + 1))) and A20: b "**" (F | ((k + 1) + 1)) = f2 . (((k + 1) + 1) - 1) by A17, Def8; defpred S2[ Nat] means ( $1 < k + 1 implies f1 . $1 = f2 . $1 ); A21: for m being Nat st S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A22: S2[m] ; ::_thesis: S2[m + 1] set m1 = m + 1; assume A23: m + 1 < k + 1 ; ::_thesis: f1 . (m + 1) = f2 . (m + 1) k + 1 < dom F by A5, NAT_1:44; then m + 1 < dom F by A23, XXREAL_0:2; then A24: m + 1 in dom F by NAT_1:44; m + 1 < (k + 1) + 1 by A23, NAT_1:13; then m + 1 in (k + 1) + 1 by NAT_1:44; then m + 1 in (dom F) /\ ((k + 1) + 1) by A24, XBOOLE_0:def_4; then m + 1 in dom (F | ((k + 1) + 1)) by RELAT_1:61; then A25: (F | ((k + 1) + 1)) . (m + 1) = F . (m + 1) by FUNCT_1:47; m + 1 in k + 1 by A23, NAT_1:44; then m + 1 in (dom F) /\ (k + 1) by A24, XBOOLE_0:def_4; then m + 1 in dom (F | (k + 1)) by RELAT_1:61; then A26: (F | (k + 1)) . (m + 1) = F . (m + 1) by FUNCT_1:47; m + 1 < len (F | ((k + 1) + 1)) by A17, A23, NAT_1:13; then f2 . (m + 1) = b . ((f1 . m),((F | (k + 1)) . (m + 1))) by A19, A22, A23, A26, A25, NAT_1:13; hence f1 . (m + 1) = f2 . (m + 1) by A13, A15, A23; ::_thesis: verum end; 0 in (k + 1) + 1 by NAT_1:44; then 0 in (dom F) /\ ((k + 1) + 1) by A7, XBOOLE_0:def_4; then 0 in dom (F | ((k + 1) + 1)) by RELAT_1:61; then A27: S2[ 0 ] by A14, A18, A8, FUNCT_1:47; for m being Nat holds S2[m] from NAT_1:sch_2(A27, A21); then A28: ( (dom F) /\ ((k + 1) + 1) = dom (F | ((k + 1) + 1)) & f1 . k = f2 . k ) by A9, RELAT_1:61; k + 1 < (k + 1) + 1 by NAT_1:13; then f2 . (k + 1) = b . ((f2 . k),((F | ((k + 1) + 1)) . (k + 1))) by A17, A19; hence b . ((b "**" (F | (k + 1))),(F . (k + 1))) = b "**" (F | ((k + 1) + 1)) by A16, A20, A10, A28, FUNCT_1:47; ::_thesis: verum end; A29: S1[ 0 ] proof assume that A30: 0 in dom F and A31: ( b is having_a_unity or len (F | 0) >= 1 ) ; ::_thesis: b . ((b "**" (F | 0)),(F . 0)) = b "**" (F | (0 + 1)) A32: F . 0 in rng F by A30, FUNCT_1:def_3; len F > 0 by A30; then A33: len (F | 1) = 1 by AFINSQ_1:54, NAT_1:14; then A34: F | 1 = <%((F | 1) . 0)%> by AFINSQ_1:34; 0 in 1 by NAT_1:44; then A35: F . 0 = (F | 1) . 0 by A33, FUNCT_1:47; len (F | 0) = 0 ; then b "**" (F | 0) = the_unity_wrt b by A31, Def8; then b . ((b "**" (F | 0)),(F . 0)) = F . 0 by A31, A32, SETWISEO:15; hence b . ((b "**" (F | 0)),(F . 0)) = b "**" (F | (0 + 1)) by A32, A34, A35, Th37; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A29, A4); hence b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) by A1, A2, A3, NAT_1:14; ::_thesis: verum end; theorem Th44: :: AFINSQ_2:44 for D being non empty set for F being XFinSequence of D for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds b "**" F = b "**" (XFS2FS F) proof let D be non empty set ; ::_thesis: for F being XFinSequence of D for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds b "**" F = b "**" (XFS2FS F) let F be XFinSequence of D; ::_thesis: for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds b "**" F = b "**" (XFS2FS F) let b be BinOp of D; ::_thesis: ( ( b is having_a_unity or len F >= 1 ) implies b "**" F = b "**" (XFS2FS F) ) assume A1: ( b is having_a_unity or len F >= 1 ) ; ::_thesis: b "**" F = b "**" (XFS2FS F) percases ( len F >= 1 or ( b is having_a_unity & len F < 1 ) ) by A1; supposeA2: len F >= 1 ; ::_thesis: b "**" F = b "**" (XFS2FS F) set FS = XFS2FS F; len F = len (XFS2FS F) by AFINSQ_1:def_9; then consider f being Function of NAT,D such that A3: f . 1 = (XFS2FS F) . 1 and A4: for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = b . ((f . n),((XFS2FS F) . (n + 1))) and A5: b "**" (XFS2FS F) = f . (len F) by A2, FINSOP_1:def_1; consider xf being Function of NAT,D such that A6: xf . 0 = F . 0 and A7: for n being Nat st n + 1 < len F holds xf . (n + 1) = b . ((xf . n),(F . (n + 1))) and A8: b "**" F = xf . ((len F) - 1) by A2, Def8; defpred S1[ Nat] means ( $1 < len F implies xf . $1 = f . ($1 + 1) ); A9: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A10: S1[n] ; ::_thesis: S1[n + 1] set n1 = n + 1; set n2 = (n + 1) + 1; assume A11: n + 1 < len F ; ::_thesis: xf . (n + 1) = f . ((n + 1) + 1) then ( 0 + 1 <= (n + 1) + 1 & (n + 1) + 1 <= len F ) by NAT_1:13; then A12: F . (((n + 1) + 1) -' 1) = (XFS2FS F) . ((n + 1) + 1) by AFINSQ_1:def_9; ( xf . (n + 1) = b . ((xf . n),(F . (n + 1))) & f . ((n + 1) + 1) = b . ((f . (n + 1)),((XFS2FS F) . ((n + 1) + 1))) ) by A7, A4, A11; hence xf . (n + 1) = f . ((n + 1) + 1) by A10, A11, A12, NAT_1:13, NAT_D:34; ::_thesis: verum end; reconsider L1 = (len F) - 1 as Element of NAT by A2, NAT_1:21; A13: L1 < L1 + 1 by NAT_1:13; A14: S1[ 0 ] proof assume 0 < len F ; ::_thesis: xf . 0 = f . (0 + 1) then 0 + 1 <= len F by NAT_1:13; then F . (1 -' 1) = (XFS2FS F) . 1 by AFINSQ_1:def_9; hence xf . 0 = f . (0 + 1) by A6, A3, XREAL_1:232; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A14, A9); hence b "**" F = b "**" (XFS2FS F) by A8, A5, A13; ::_thesis: verum end; supposeA15: ( b is having_a_unity & len F < 1 ) ; ::_thesis: b "**" F = b "**" (XFS2FS F) then len F <= 0 + 1 ; then A16: len F = 0 by A15, NAT_1:8; then ( len F = len (XFS2FS F) & b "**" F = the_unity_wrt b ) by A15, Def8, AFINSQ_1:def_9; hence b "**" F = b "**" (XFS2FS F) by A15, A16, FINSOP_1:def_1; ::_thesis: verum end; end; end; theorem Th45: :: AFINSQ_2:45 for D being non empty set for F, G being XFinSequence of D for b being BinOp of D for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds b "**" F = b "**" G proof let D be non empty set ; ::_thesis: for F, G being XFinSequence of D for b being BinOp of D for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds b "**" F = b "**" G let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds b "**" F = b "**" G let b be BinOp of D; ::_thesis: for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds b "**" F = b "**" G let P be Permutation of (dom F); ::_thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P implies b "**" F = b "**" G ) assume that A1: ( b is commutative & b is associative ) and A2: ( b is having_a_unity or len F >= 1 ) and A3: G = F * P ; ::_thesis: b "**" F = b "**" G set xF = XFS2FS F; A4: ( b is having_a_unity or len (XFS2FS F) >= 1 ) by A2, AFINSQ_1:def_9; set xG = XFS2FS G; defpred S1[ set , set ] means for n being Nat st $1 = n holds $2 = (P . (n - 1)) + 1; dom F = len F ; then reconsider d = dom F as Element of NAT ; A5: for x being set st x in Seg d holds ex y being set st ( y in Seg d & S1[x,y] ) proof let x be set ; ::_thesis: ( x in Seg d implies ex y being set st ( y in Seg d & S1[x,y] ) ) assume A6: x in Seg d ; ::_thesis: ex y being set st ( y in Seg d & S1[x,y] ) reconsider x9 = x as Element of NAT by A6; 1 + 0 <= x9 by A6, FINSEQ_1:1; then reconsider x91 = x9 - 1 as Element of NAT by NAT_1:21; A7: x91 + 1 <= d by A6, FINSEQ_1:1; then x91 < d by NAT_1:13; then A8: x91 in d by NAT_1:44; take (P . x91) + 1 ; ::_thesis: ( (P . x91) + 1 in Seg d & S1[x,(P . x91) + 1] ) dom F = dom P by A7, FUNCT_2:def_1; then P . x91 in rng P by A8, FUNCT_1:def_3; then P . x91 < d by NAT_1:44; then ( 0 + 1 <= (P . x91) + 1 & (P . x91) + 1 <= d ) by NAT_1:13; hence ( (P . x91) + 1 in Seg d & S1[x,(P . x91) + 1] ) by FINSEQ_1:1; ::_thesis: verum end; consider P9 being Function of (Seg d),(Seg d) such that A9: for x being set st x in Seg d holds S1[x,P9 . x] from FUNCT_2:sch_1(A5); now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_P9_&_x2_in_dom_P9_&_P9_._x1_=_P9_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 implies x1 = x2 ) assume that A10: x1 in dom P9 and A11: x2 in dom P9 and A12: P9 . x1 = P9 . x2 ; ::_thesis: x1 = x2 dom P9 = Seg d by FUNCT_2:52; then reconsider X1 = x1, X2 = x2 as Element of NAT by A10, A11; ( 1 + 0 <= X1 & 1 + 0 <= X2 ) by A10, A11, FINSEQ_1:1; then reconsider X19 = X1 - 1, X29 = X2 - 1 as Element of NAT by NAT_1:21; A13: ( X19 < X19 + 1 & X1 <= d ) by A10, FINSEQ_1:1, NAT_1:13; then A14: dom P = dom F by FUNCT_2:def_1; ( X29 < X29 + 1 & X2 <= d ) by A11, FINSEQ_1:1, NAT_1:13; then X29 < d by XXREAL_0:2; then A15: X29 in dom P by A14, NAT_1:44; X19 < d by A13, XXREAL_0:2; then A16: X19 in dom P by A14, NAT_1:44; P9 . X1 = (P . X19) + 1 by A9, A10; then ((P . X19) + 1) - 1 = ((P . X29) + 1) - 1 by A9, A11, A12; then (X1 - 1) + 1 = (X2 - 1) + 1 by A16, A15, FUNCT_1:def_4; hence x1 = x2 ; ::_thesis: verum end; then A17: P9 is one-to-one by FUNCT_1:def_4; card (Seg d) = card (Seg d) ; then A18: ( P9 is one-to-one & P9 is onto ) by A17, Lm2; len (XFS2FS F) = len F by AFINSQ_1:def_9; then dom (XFS2FS F) = Seg (len F) by FINSEQ_1:def_3; then reconsider P9 = P9 as Permutation of (dom (XFS2FS F)) by A18; A19: ( dom P9 = Seg d & dom (XFS2FS G) = Seg (len (XFS2FS G)) ) by FINSEQ_1:def_3, FUNCT_2:52; rng P9 c= dom (XFS2FS F) ; then A20: dom ((XFS2FS F) * P9) = dom P9 by RELAT_1:27; rng P c= dom F ; then dom (F * P) = dom P by RELAT_1:27; then A21: dom G = dom F by A3, FUNCT_2:52; A22: dom G = len G ; A23: for x9 being set st x9 in dom (XFS2FS G) holds (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 proof let x9 be set ; ::_thesis: ( x9 in dom (XFS2FS G) implies (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 ) assume A24: x9 in dom (XFS2FS G) ; ::_thesis: (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 reconsider x = x9 as Element of NAT by A24; A25: dom (XFS2FS G) = Seg (len (XFS2FS G)) by FINSEQ_1:def_3; then A26: 1 <= x by A24, FINSEQ_1:1; then A27: x -' 1 = x - 1 by XREAL_1:233; 0 < x by A24, A25, FINSEQ_1:1; then reconsider x1 = x - 1 as Element of NAT by NAT_1:20; A28: dom (XFS2FS F) = Seg (len (XFS2FS F)) by FINSEQ_1:def_3; A29: len (XFS2FS G) = len G by AFINSQ_1:def_9; then A30: ( (P . (x - 1)) + 1 = P9 . x & x in dom P9 ) by A9, A21, A24, A25, FUNCT_2:52; then A31: (P . (x - 1)) + 1 in rng P9 by FUNCT_1:def_3; A32: x <= len F by A21, A24, A25, A29, FINSEQ_1:1; then A33: (XFS2FS G) . x = (F * P) . (x -' 1) by A3, A21, A22, A26, AFINSQ_1:def_9; len (XFS2FS F) = len F by AFINSQ_1:def_9; then A34: (P . (x - 1)) + 1 <= len F by A31, A28, FINSEQ_1:1; ( x1 < x1 + 1 & x -' 1 = x1 ) by A26, NAT_1:13, XREAL_1:233; then x -' 1 < dom G by A21, A32, XXREAL_0:2; then x -' 1 in dom G by NAT_1:44; then A35: ( ((P . (x -' 1)) + 1) -' 1 = P . (x -' 1) & (F * P) . (x -' 1) = F . (P . (x -' 1)) ) by A3, FUNCT_1:12, NAT_D:34; 1 <= (P . (x - 1)) + 1 by A31, A28, FINSEQ_1:1; then (F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1) by A34, A27, A35, AFINSQ_1:def_9; hence (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 by A30, A33, FUNCT_1:13; ::_thesis: verum end; len (XFS2FS G) = len F by A21, A22, AFINSQ_1:def_9; then XFS2FS G = (XFS2FS F) * P9 by A23, A20, A19, FUNCT_1:def_11; then A36: b "**" (XFS2FS G) = b "**" (XFS2FS F) by A1, A4, FINSOP_1:7; b "**" (XFS2FS G) = b "**" G by A2, A21, A22, Th44; hence b "**" F = b "**" G by A2, A36, Th44; ::_thesis: verum end; theorem :: AFINSQ_2:46 for D being non empty set for F, G being XFinSequence of D for b being BinOp of D for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ) holds b "**" (F ^ G) = b "**" bFG proof let D be non empty set ; ::_thesis: for F, G being XFinSequence of D for b being BinOp of D for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ) holds b "**" (F ^ G) = b "**" bFG let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ) holds b "**" (F ^ G) = b "**" bFG let b be BinOp of D; ::_thesis: for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ) holds b "**" (F ^ G) = b "**" bFG let bFG be XFinSequence of D; ::_thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ) implies b "**" (F ^ G) = b "**" bFG ) assume that A1: ( b is commutative & b is associative ) and A2: ( b is having_a_unity or len F >= 1 ) and A3: len F = len G and A4: len F = len bFG and A5: for n being Nat st n in dom bFG holds bFG . n = b . ((F . n),(G . n)) ; ::_thesis: b "**" (F ^ G) = b "**" bFG set xG = XFS2FS G; set xF = XFS2FS F; A6: ( b "**" F = b "**" (XFS2FS F) & b "**" G = b "**" (XFS2FS G) ) by A2, A3, Th44; set xb = XFS2FS bFG; A7: len (XFS2FS bFG) = len bFG by AFINSQ_1:def_9; A8: for k being Element of NAT st k in dom (XFS2FS bFG) holds (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) proof let k be Element of NAT ; ::_thesis: ( k in dom (XFS2FS bFG) implies (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) ) assume A9: k in dom (XFS2FS bFG) ; ::_thesis: (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3; then k >= 1 by FINSEQ_1:1; then reconsider k1 = k - 1 as Element of NAT by NAT_1:21; A10: k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3; then A11: 1 <= k by FINSEQ_1:1; then A12: k1 = k -' 1 by XREAL_1:233; k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3; then ( k1 < k1 + 1 & k <= len (XFS2FS bFG) ) by FINSEQ_1:1, NAT_1:13; then k1 < len (XFS2FS bFG) by XXREAL_0:2; then k1 in dom bFG by A7, NAT_1:44; then A13: bFG . k1 = b . ((F . k1),(G . k1)) by A5; A14: k <= len bFG by A7, A10, FINSEQ_1:1; then ( bFG . (k -' 1) = (XFS2FS bFG) . k & F . (k -' 1) = (XFS2FS F) . k ) by A4, A11, AFINSQ_1:def_9; hence (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) by A3, A4, A11, A14, A13, A12, AFINSQ_1:def_9; ::_thesis: verum end; ( len (XFS2FS F) = len F & len G = len (XFS2FS G) ) by AFINSQ_1:def_9; then b "**" (XFS2FS bFG) = b . ((b "**" (XFS2FS F)),(b "**" (XFS2FS G))) by A1, A2, A3, A4, A7, A8, FINSOP_1:9; then b "**" bFG = b . ((b "**" F),(b "**" G)) by A2, A4, A6, Th44; hence b "**" (F ^ G) = b "**" bFG by A1, A2, A3, Th42; ::_thesis: verum end; theorem Th47: :: AFINSQ_2:47 for D being non empty set for F being XFinSequence of D for D1, D2 being non empty set for b1 being BinOp of D1 for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds b1 "**" F = b2 "**" F proof let D be non empty set ; ::_thesis: for F being XFinSequence of D for D1, D2 being non empty set for b1 being BinOp of D1 for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds b1 "**" F = b2 "**" F let F be XFinSequence of D; ::_thesis: for D1, D2 being non empty set for b1 being BinOp of D1 for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds b1 "**" F = b2 "**" F let D1, D2 be non empty set ; ::_thesis: for b1 being BinOp of D1 for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds b1 "**" F = b2 "**" F let b1 be BinOp of D1; ::_thesis: for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds b1 "**" F = b2 "**" F let b2 be BinOp of D2; ::_thesis: ( len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) implies b1 "**" F = b2 "**" F ) assume that A1: len F >= 1 and A2: D c= D1 /\ D2 and A3: for x, y being set st x in D & y in D holds ( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ; ::_thesis: b1 "**" F = b2 "**" F ( D1 /\ D2 c= D1 & D1 /\ D2 c= D2 ) by XBOOLE_1:17; then A4: ( D c= D1 & D c= D2 ) by A2, XBOOLE_1:1; ( rng F c= D1 & rng F c= D2 ) by A4, XBOOLE_1:1; then A5: ( F is D1 -valued & F is D2 -valued ) by RELAT_1:def_19; then consider F1 being Function of NAT,D1 such that A6: F1 . 0 = F . 0 and A7: for n being Nat st n + 1 < len F holds F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1))) and A8: b1 "**" F = F1 . ((len F) - 1) by A1, Def8; consider F2 being Function of NAT,D2 such that A9: F2 . 0 = F . 0 and A10: for n being Nat st n + 1 < len F holds F2 . (n + 1) = b2 . ((F2 . n),(F . (n + 1))) and A11: b2 "**" F = F2 . ((len F) - 1) by A1, Def8, A5; defpred S1[ Nat] means ( $1 < len F implies ( F1 . $1 = F2 . $1 & F1 . $1 in D ) ); 0 in dom F by A1, NAT_1:44; then F . 0 in rng F by FUNCT_1:def_3; then A12: S1[ 0 ] by A6, A9; A13: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A14: S1[n] ; ::_thesis: S1[n + 1] assume A15: n + 1 < len F ; ::_thesis: ( F1 . (n + 1) = F2 . (n + 1) & F1 . (n + 1) in D ) then ( n + 1 in dom F & n < len F ) by NAT_1:13, NAT_1:44; then A16: ( F . (n + 1) in rng F & n in dom F ) by FUNCT_1:def_3, NAT_1:44; A17: F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1))) by A7, A15; then F1 . (n + 1) = b2 . ((F2 . n),(F . (n + 1))) by A3, A16, A14, NAT_1:44 .= F2 . (n + 1) by A10, A15 ; hence ( F1 . (n + 1) = F2 . (n + 1) & F1 . (n + 1) in D ) by A16, A14, A17, A3, NAT_1:44; ::_thesis: verum end; reconsider l1 = (len F) - 1 as Element of NAT by A1, NAT_1:21; A18: l1 < l1 + 1 by NAT_1:13; for n being Nat holds S1[n] from NAT_1:sch_2(A12, A13); hence b1 "**" F = b2 "**" F by A8, A11, A18; ::_thesis: verum end; Lm3: for cF being complex-valued XFinSequence holds cF is COMPLEX -valued proof let cF be complex-valued XFinSequence; ::_thesis: cF is COMPLEX -valued rng cF c= COMPLEX by VALUED_0:def_1; hence cF is COMPLEX -valued by RELAT_1:def_19; ::_thesis: verum end; Lm4: for rF being real-valued XFinSequence holds rF is REAL -valued proof let rF be real-valued XFinSequence; ::_thesis: rF is REAL -valued rng rF c= REAL by VALUED_0:def_3; hence rF is REAL -valued by RELAT_1:def_19; ::_thesis: verum end; definition let F be XFinSequence; func Sum F -> Element of COMPLEX equals :: AFINSQ_2:def 9 addcomplex "**" F; coherence addcomplex "**" F is Element of COMPLEX ; end; :: deftheorem defines Sum AFINSQ_2:def_9_:_ for F being XFinSequence holds Sum F = addcomplex "**" F; registration let f be empty complex-valued XFinSequence; cluster Sum f -> zero ; coherence Sum f is empty proof ( f is COMPLEX -valued & len f = 0 ) by Lm3; hence Sum f is empty by Def8, BINOP_2:1; ::_thesis: verum end; end; theorem Th48: :: AFINSQ_2:48 for F being XFinSequence st F is real-valued holds Sum F = addreal "**" F proof let F be XFinSequence; ::_thesis: ( F is real-valued implies Sum F = addreal "**" F ) assume A1: F is real-valued ; ::_thesis: Sum F = addreal "**" F then rng F c= REAL by VALUED_0:def_3; then A2: F is REAL -valued by RELAT_1:def_19; rng F c= COMPLEX by A1, MEMBERED:1; then A3: F is COMPLEX -valued by RELAT_1:def_19; percases ( len F = 0 or len F >= 1 ) by NAT_1:14; supposeA4: len F = 0 ; ::_thesis: Sum F = addreal "**" F hence addreal "**" F = 0 by Def8, A2, BINOP_2:2 .= Sum F by Def8, A3, A4, BINOP_2:1 ; ::_thesis: verum end; supposeA5: len F >= 1 ; ::_thesis: Sum F = addreal "**" F A6: REAL = REAL /\ COMPLEX by MEMBERED:1, XBOOLE_1:28; now__::_thesis:_for_x,_y_being_set_st_x_in_REAL_&_y_in_REAL_holds_ (_addreal_._(x,y)_=_addcomplex_._(x,y)_&_addreal_._(x,y)_in_REAL_) let x, y be set ; ::_thesis: ( x in REAL & y in REAL implies ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL ) ) assume ( x in REAL & y in REAL ) ; ::_thesis: ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL ) then reconsider X = x, Y = y as Element of REAL ; addreal . (x,y) = X + Y by BINOP_2:def_9; hence ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL ) by BINOP_2:def_3; ::_thesis: verum end; hence Sum F = addreal "**" F by Th47, A5, A6, A2; ::_thesis: verum end; end; end; theorem Th49: :: AFINSQ_2:49 for F being XFinSequence st F is RAT -valued holds Sum F = addrat "**" F proof let F be XFinSequence; ::_thesis: ( F is RAT -valued implies Sum F = addrat "**" F ) assume A1: F is RAT -valued ; ::_thesis: Sum F = addrat "**" F rng F c= COMPLEX by A1, MEMBERED:1; then A2: F is COMPLEX -valued by RELAT_1:def_19; percases ( len F = 0 or len F >= 1 ) by NAT_1:14; supposeA3: len F = 0 ; ::_thesis: Sum F = addrat "**" F hence addrat "**" F = 0 by Def8, A1, BINOP_2:3 .= Sum F by Def8, A2, A3, BINOP_2:1 ; ::_thesis: verum end; supposeA4: len F >= 1 ; ::_thesis: Sum F = addrat "**" F A5: RAT = RAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28; now__::_thesis:_for_x,_y_being_set_st_x_in_RAT_&_y_in_RAT_holds_ (_addrat_._(x,y)_=_addcomplex_._(x,y)_&_addrat_._(x,y)_in_RAT_) let x, y be set ; ::_thesis: ( x in RAT & y in RAT implies ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) ) assume ( x in RAT & y in RAT ) ; ::_thesis: ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) then reconsider X = x, Y = y as Element of RAT ; addrat . (x,y) = X + Y by BINOP_2:def_15; hence ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) by BINOP_2:def_3; ::_thesis: verum end; hence Sum F = addrat "**" F by Th47, A4, A5, A1; ::_thesis: verum end; end; end; theorem Th50: :: AFINSQ_2:50 for F being XFinSequence st F is INT -valued holds Sum F = addint "**" F proof let F be XFinSequence; ::_thesis: ( F is INT -valued implies Sum F = addint "**" F ) assume A1: F is INT -valued ; ::_thesis: Sum F = addint "**" F rng F c= COMPLEX by A1, MEMBERED:1; then A2: F is COMPLEX -valued by RELAT_1:def_19; percases ( len F = 0 or len F >= 1 ) by NAT_1:14; supposeA3: len F = 0 ; ::_thesis: Sum F = addint "**" F hence addint "**" F = 0 by Def8, A1, BINOP_2:4 .= Sum F by Def8, A2, A3, BINOP_2:1 ; ::_thesis: verum end; supposeA4: len F >= 1 ; ::_thesis: Sum F = addint "**" F A5: INT = INT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28; now__::_thesis:_for_x,_y_being_set_st_x_in_INT_&_y_in_INT_holds_ (_addint_._(x,y)_=_addcomplex_._(x,y)_&_addint_._(x,y)_in_INT_) let x, y be set ; ::_thesis: ( x in INT & y in INT implies ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT ) ) assume ( x in INT & y in INT ) ; ::_thesis: ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT ) then reconsider X = x, Y = y as Element of INT ; addint . (x,y) = X + Y by BINOP_2:def_20; hence ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT ) by BINOP_2:def_3; ::_thesis: verum end; hence Sum F = addint "**" F by Th47, A4, A5, A1; ::_thesis: verum end; end; end; theorem Th51: :: AFINSQ_2:51 for F being XFinSequence st F is natural-valued holds Sum F = addnat "**" F proof let F be XFinSequence; ::_thesis: ( F is natural-valued implies Sum F = addnat "**" F ) assume A1: F is natural-valued ; ::_thesis: Sum F = addnat "**" F then rng F c= NAT by VALUED_0:def_6; then A2: F is NAT -valued by RELAT_1:def_19; rng F c= COMPLEX by A1, MEMBERED:1; then A3: F is COMPLEX -valued by RELAT_1:def_19; percases ( len F = 0 or len F >= 1 ) by NAT_1:14; supposeA4: len F = 0 ; ::_thesis: Sum F = addnat "**" F hence addnat "**" F = 0 by Def8, A2, BINOP_2:5 .= Sum F by Def8, A3, A4, BINOP_2:1 ; ::_thesis: verum end; supposeA5: len F >= 1 ; ::_thesis: Sum F = addnat "**" F A6: NAT = NAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28; now__::_thesis:_for_x,_y_being_set_st_x_in_NAT_&_y_in_NAT_holds_ (_addnat_._(x,y)_=_addcomplex_._(x,y)_&_addnat_._(x,y)_in_NAT_) let x, y be set ; ::_thesis: ( x in NAT & y in NAT implies ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT ) ) assume ( x in NAT & y in NAT ) ; ::_thesis: ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT ) then reconsider X = x, Y = y as Element of NAT ; addnat . (x,y) = X + Y by BINOP_2:def_23; hence ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT ) by BINOP_2:def_3; ::_thesis: verum end; hence Sum F = addnat "**" F by Th47, A5, A6, A2; ::_thesis: verum end; end; end; registration let F be real-valued XFinSequence; cluster Sum F -> real ; coherence Sum F is real proof Sum F = addreal "**" F by Th48; hence Sum F is real ; ::_thesis: verum end; end; registration let F be RAT -valued XFinSequence; cluster Sum F -> rational ; coherence Sum F is rational proof Sum F = addrat "**" F by Th49; hence Sum F is rational ; ::_thesis: verum end; end; registration let F be INT -valued XFinSequence; cluster Sum F -> integer ; coherence Sum F is integer proof Sum F = addint "**" F by Th50; hence Sum F is integer ; ::_thesis: verum end; end; registration let F be natural-valued XFinSequence; cluster Sum F -> natural ; coherence Sum F is natural proof Sum F = addnat "**" F by Th51; hence Sum F is natural ; ::_thesis: verum end; end; registration cluster Relation-like natural-valued -> nonnegative-yielding for set ; coherence for b1 being Relation st b1 is natural-valued holds b1 is nonnegative-yielding proof let R be Relation; ::_thesis: ( R is natural-valued implies R is nonnegative-yielding ) assume R is natural-valued ; ::_thesis: R is nonnegative-yielding then for r being real number st r in rng R holds r >= 0 ; hence R is nonnegative-yielding by PARTFUN3:def_4; ::_thesis: verum end; end; theorem :: AFINSQ_2:52 for cF being complex-valued XFinSequence st cF = {} holds Sum cF = 0 ; theorem :: AFINSQ_2:53 for c being complex number holds Sum <%c%> = c proof let c be complex number ; ::_thesis: Sum <%c%> = c c in COMPLEX by XCMPLX_0:def_2; hence Sum <%c%> = c by Th37; ::_thesis: verum end; theorem :: AFINSQ_2:54 for c1, c2 being complex number holds Sum <%c1,c2%> = c1 + c2 proof let c1, c2 be complex number ; ::_thesis: Sum <%c1,c2%> = c1 + c2 ( c1 in COMPLEX & c2 in COMPLEX ) by XCMPLX_0:def_2; then addcomplex "**" <%c1,c2%> = addcomplex . (c1,c2) by Th38 .= c1 + c2 by BINOP_2:def_3 ; hence Sum <%c1,c2%> = c1 + c2 ; ::_thesis: verum end; theorem Th55: :: AFINSQ_2:55 for cF1, cF2 being complex-valued XFinSequence holds Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2) proof let cF1, cF2 be complex-valued XFinSequence; ::_thesis: Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2) A1: ( cF1 is COMPLEX -valued & cF2 is COMPLEX -valued ) by Lm3; thus Sum (cF1 ^ cF2) = addcomplex . ((Sum cF1),(Sum cF2)) by Th42, A1 .= (Sum cF1) + (Sum cF2) by BINOP_2:def_3 ; ::_thesis: verum end; theorem :: AFINSQ_2:56 for n being Nat for rF being real-valued XFinSequence for S being Real_Sequence st rF = S | (n + 1) holds Sum rF = (Partial_Sums S) . n proof let n be Nat; ::_thesis: for rF being real-valued XFinSequence for S being Real_Sequence st rF = S | (n + 1) holds Sum rF = (Partial_Sums S) . n let rF be real-valued XFinSequence; ::_thesis: for S being Real_Sequence st rF = S | (n + 1) holds Sum rF = (Partial_Sums S) . n let S be Real_Sequence; ::_thesis: ( rF = S | (n + 1) implies Sum rF = (Partial_Sums S) . n ) A1: rF is REAL -valued by Lm4; n + 1 c= NAT by ORDINAL1:def_2; then A2: n + 1 c= dom S by FUNCT_2:def_1; assume A3: rF = S | (n + 1) ; ::_thesis: Sum rF = (Partial_Sums S) . n then dom rF = (dom S) /\ (n + 1) by RELAT_1:61; then A4: dom rF = n + 1 by A2, XBOOLE_1:28; then consider f being Function of NAT,REAL such that A5: f . 0 = rF . 0 and A6: for m being Nat st m + 1 < len rF holds f . (m + 1) = addreal . ((f . m),(rF . (m + 1))) and A7: addreal "**" rF = f . ((len rF) - 1) by Def8, A1; defpred S1[ Nat] means ( $1 in dom rF implies f . $1 = (Partial_Sums S) . $1 ); A8: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A9: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof assume A10: k + 1 in dom rF ; ::_thesis: f . (k + 1) = (Partial_Sums S) . (k + 1) then A11: k + 1 < len rF by NAT_1:44; then A12: k < len rF by NAT_1:13; A13: k in NAT by ORDINAL1:def_12; thus f . (k + 1) = addreal . ((f . k),(rF . (k + 1))) by A6, A11 .= (f . k) + (rF . (k + 1)) by BINOP_2:def_9 .= (f . k) + (S . (k + 1)) by A3, A10, FUNCT_1:47 .= (Partial_Sums S) . (k + 1) by A9, A12, A13, NAT_1:44, SERIES_1:def_1 ; ::_thesis: verum end; end; (Partial_Sums S) . 0 = S . 0 by SERIES_1:def_1; then A14: S1[ 0 ] by A3, A5, FUNCT_1:47; for m being Nat holds S1[m] from NAT_1:sch_2(A14, A8); hence (Partial_Sums S) . n = f . n by A4, NAT_1:45 .= Sum rF by Th48, A7, A4 ; ::_thesis: verum end; theorem Th57: :: AFINSQ_2:57 for rF1, rF2 being real-valued XFinSequence st len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds rF1 . i <= rF2 . i ) holds Sum rF1 <= Sum rF2 proof let rF1, rF2 be real-valued XFinSequence; ::_thesis: ( len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds rF1 . i <= rF2 . i ) implies Sum rF1 <= Sum rF2 ) set d = rF1; set e = rF2; assume that A1: len rF1 = len rF2 and A2: for i being Nat st i in dom rF1 holds rF1 . i <= rF2 . i ; ::_thesis: Sum rF1 <= Sum rF2 reconsider d = rF1, e = rF2 as XFinSequence of REAL by Lm4; A3: ( Sum d = addreal "**" d & Sum e = addreal "**" e ) by Th48; percases ( len d >= 1 or len d = 0 ) by NAT_1:14; supposeA4: len d >= 1 ; ::_thesis: Sum rF1 <= Sum rF2 consider f being Function of NAT,REAL such that A5: f . 0 = d . 0 and A6: for n being Nat st n + 1 < len d holds f . (n + 1) = addreal . ((f . n),(d . (n + 1))) and A7: Sum d = f . ((len d) - 1) by A4, Def8, A3; consider g being Function of NAT,REAL such that A8: g . 0 = e . 0 and A9: for n being Nat st n + 1 < len e holds g . (n + 1) = addreal . ((g . n),(e . (n + 1))) and A10: Sum e = g . ((len e) - 1) by A4, A1, Def8, A3; defpred S1[ Nat] means ( $1 in dom d implies f . $1 <= g . $1 ); A11: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A12: S1[i] ; ::_thesis: S1[i + 1] thus S1[i + 1] ::_thesis: verum proof assume A13: i + 1 in dom d ; ::_thesis: f . (i + 1) <= g . (i + 1) then A14: i + 1 < len d by NAT_1:44; then A15: i < len d by NAT_1:13; A16: d . (i + 1) <= e . (i + 1) by A2, A13; A17: f . (i + 1) = addreal . ((f . i),(d . (i + 1))) by A6, A14 .= (f . i) + (d . (i + 1)) by BINOP_2:def_9 ; g . (i + 1) = addreal . ((g . i),(e . (i + 1))) by A1, A9, A14 .= (g . i) + (e . (i + 1)) by BINOP_2:def_9 ; hence f . (i + 1) <= g . (i + 1) by A12, A15, A17, A16, NAT_1:44, XREAL_1:7; ::_thesis: verum end; end; reconsider ld = (len d) - 1 as Element of NAT by A4, NAT_1:21; (len d) - 1 < (len d) - 0 by XREAL_1:10; then A18: ld in len d by NAT_1:44; A19: S1[ 0 ] by A2, A5, A8; for i being Nat holds S1[i] from NAT_1:sch_2(A19, A11); hence Sum rF1 <= Sum rF2 by A1, A7, A10, A18; ::_thesis: verum end; suppose len d = 0 ; ::_thesis: Sum rF1 <= Sum rF2 then ( Sum d = the_unity_wrt addreal & Sum e = the_unity_wrt addreal ) by Def8, A3, A1; hence Sum rF1 <= Sum rF2 ; ::_thesis: verum end; end; end; theorem Th58: :: AFINSQ_2:58 for n being Nat for c being complex number holds Sum (n --> c) = n * c proof let n be Nat; ::_thesis: for c being complex number holds Sum (n --> c) = n * c let c be complex number ; ::_thesis: Sum (n --> c) = n * c set Fn = n --> c; reconsider Fn = n --> c as XFinSequence of COMPLEX by Lm3; A1: dom Fn = n by FUNCOP_1:13; now__::_thesis:_Sum_(n_-->_c)_=_n_*_c percases ( dom Fn = 0 or dom Fn > 0 ) ; suppose dom Fn = 0 ; ::_thesis: Sum (n --> c) = n * c hence Sum (n --> c) = n * c by A1; ::_thesis: verum end; supposeA2: dom Fn > 0 ; ::_thesis: Sum (n --> c) = n * c then consider f being Function of NAT,COMPLEX such that A3: f . 0 = Fn . 0 and A4: for k being Nat st k + 1 < len Fn holds f . (k + 1) = addcomplex . ((f . k),(Fn . (k + 1))) and A5: Sum Fn = f . ((len Fn) - 1) by Def8; defpred S1[ Nat] means ( $1 < len Fn implies f . $1 = ($1 + 1) * c ); A6: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A7: S1[m] ; ::_thesis: S1[m + 1] assume A8: m + 1 < len Fn ; ::_thesis: f . (m + 1) = ((m + 1) + 1) * c then f . (m + 1) = addcomplex . ((f . m),(Fn . (m + 1))) by A4; then A9: f . (m + 1) = (f . m) + (Fn . (m + 1)) by BINOP_2:def_3; m + 1 in len Fn by A8, NAT_1:44; then Fn . (m + 1) = c by A1, FUNCOP_1:7; hence f . (m + 1) = ((m + 1) + 1) * c by A7, A8, A9, NAT_1:13; ::_thesis: verum end; reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A2, NAT_1:20; A10: lenFn1 < lenFn1 + 1 by NAT_1:13; A11: S1[ 0 ] proof assume 0 < len Fn ; ::_thesis: f . 0 = (0 + 1) * c then 0 in dom Fn by NAT_1:44; hence f . 0 = (0 + 1) * c by A3, A1, FUNCOP_1:7; ::_thesis: verum end; for m being Nat holds S1[m] from NAT_1:sch_2(A11, A6); hence Sum (n --> c) = n * c by A5, A10, A1; ::_thesis: verum end; end; end; hence Sum (n --> c) = n * c ; ::_thesis: verum end; theorem :: AFINSQ_2:59 for rF being real-valued XFinSequence for r being real number st ( for n being Nat st n in dom rF holds rF . n <= r ) holds Sum rF <= (len rF) * r proof let rF be real-valued XFinSequence; ::_thesis: for r being real number st ( for n being Nat st n in dom rF holds rF . n <= r ) holds Sum rF <= (len rF) * r let r be real number ; ::_thesis: ( ( for n being Nat st n in dom rF holds rF . n <= r ) implies Sum rF <= (len rF) * r ) set L = (len rF) --> r; assume A1: for n being Nat st n in dom rF holds rF . n <= r ; ::_thesis: Sum rF <= (len rF) * r A2: len ((len rF) --> r) = len rF by FUNCOP_1:13; now__::_thesis:_for_n_being_Nat_st_n_in_dom_rF_holds_ rF_._n_<=_((len_rF)_-->_r)_._n let n be Nat; ::_thesis: ( n in dom rF implies rF . n <= ((len rF) --> r) . n ) assume n in dom rF ; ::_thesis: rF . n <= ((len rF) --> r) . n then ( rF . n <= r & ((len rF) --> r) . n = r ) by A1, FUNCOP_1:7; hence rF . n <= ((len rF) --> r) . n ; ::_thesis: verum end; then Sum rF <= Sum ((len rF) --> r) by Th57, A2; hence Sum rF <= (len rF) * r by Th58; ::_thesis: verum end; theorem :: AFINSQ_2:60 for rF being real-valued XFinSequence for r being real number st ( for n being Nat st n in dom rF holds rF . n >= r ) holds Sum rF >= (len rF) * r proof let rF be real-valued XFinSequence; ::_thesis: for r being real number st ( for n being Nat st n in dom rF holds rF . n >= r ) holds Sum rF >= (len rF) * r let r be real number ; ::_thesis: ( ( for n being Nat st n in dom rF holds rF . n >= r ) implies Sum rF >= (len rF) * r ) set L = (len rF) --> r; assume A1: for n being Nat st n in dom rF holds rF . n >= r ; ::_thesis: Sum rF >= (len rF) * r A2: len ((len rF) --> r) = len rF by FUNCOP_1:13; now__::_thesis:_for_n_being_Nat_st_n_in_dom_rF_holds_ rF_._n_>=_((len_rF)_-->_r)_._n let n be Nat; ::_thesis: ( n in dom rF implies rF . n >= ((len rF) --> r) . n ) assume n in dom rF ; ::_thesis: rF . n >= ((len rF) --> r) . n then ( rF . n >= r & ((len rF) --> r) . n = r ) by A1, FUNCOP_1:7; hence rF . n >= ((len rF) --> r) . n ; ::_thesis: verum end; then Sum rF >= Sum ((len rF) --> r) by Th57, A2; hence Sum rF >= (len rF) * r by Th58; ::_thesis: verum end; theorem Th61: :: AFINSQ_2:61 for rF being real-valued XFinSequence for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st ( x in dom rF & rF . x = r ) holds Sum rF >= r proof let rF be real-valued XFinSequence; ::_thesis: for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st ( x in dom rF & rF . x = r ) holds Sum rF >= r let r be real number ; ::_thesis: ( rF is nonnegative-yielding & len rF > 0 & ex x being set st ( x in dom rF & rF . x = r ) implies Sum rF >= r ) assume that A1: rF is nonnegative-yielding and A2: len rF > 0 and A3: ex x being set st ( x in dom rF & rF . x = r ) ; ::_thesis: Sum rF >= r consider x being set such that A4: x in dom rF and A5: rF . x = r by A3; reconsider lenrF1 = (len rF) - 1 as Element of NAT by A2, NAT_1:20; A6: dom rF = lenrF1 + 1 ; reconsider x = x as Element of NAT by A4; A7: lenrF1 < lenrF1 + 1 by NAT_1:13; A8: x < dom rF by A4, NAT_1:44; then A9: x <= lenrF1 by A6, NAT_1:13; rF is REAL -valued by Lm4; then consider f being Function of NAT,REAL such that A10: f . 0 = rF . 0 and A11: for n being Nat st n + 1 < len rF holds f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) and A12: addreal "**" rF = f . ((len rF) - 1) by Def8, A2; defpred S1[ Nat] means ( $1 < x implies f . $1 >= 0 ); 0 in len rF by A2, NAT_1:44; then rF . 0 in rng rF by FUNCT_1:def_3; then A13: S1[ 0 ] by A1, A10, PARTFUN3:def_4; A14: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A15: S1[n] ; ::_thesis: S1[n + 1] assume A16: n + 1 < x ; ::_thesis: f . (n + 1) >= 0 then ( n < x & n + 1 < len rF ) by A8, NAT_1:13, XXREAL_0:2; then A17: ( f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) & f . n >= 0 & n + 1 in dom rF ) by A11, A15, NAT_1:44; then rF . (n + 1) in rng rF by FUNCT_1:def_3; then rF . (n + 1) >= 0 by A1, PARTFUN3:def_4; then (f . n) + (rF . (n + 1)) >= 0 + 0 by A16, A15, NAT_1:13; hence f . (n + 1) >= 0 by A17, BINOP_2:def_9; ::_thesis: verum end; A18: for n being Nat holds S1[n] from NAT_1:sch_2(A13, A14); defpred S2[ Nat] means ( x <= $1 & $1 < len rF implies f . $1 >= r ); now__::_thesis:_(_x_<=_x_&_x_<_len_rF_implies_f_._x_>=_r_) percases ( x = 0 or x > 0 ) ; supposeA19: x = 0 ; ::_thesis: ( x <= x & x < len rF implies f . x >= r ) assume that x <= x and x < len rF ; ::_thesis: f . x >= r thus f . x >= r by A5, A10, A19; ::_thesis: verum end; suppose x > 0 ; ::_thesis: ( x <= x & x < len rF implies f . x >= r ) then reconsider x1 = x - 1 as Element of NAT by NAT_1:20; assume that x <= x and A20: x < len rF ; ::_thesis: f . x >= r A21: x1 < x1 + 1 by NAT_1:13; x1 + 1 < len rF by A20; then f . x = addreal . ((f . x1),(rF . x)) by A11; then ( f . x = (f . x1) + (rF . x) & f . x1 >= 0 ) by A21, A18, BINOP_2:def_9; then f . x >= r + 0 by A5, XREAL_1:7; hence f . x >= r ; ::_thesis: verum end; end; end; then A22: S2[x] ; A23: for m being Nat st m >= x & S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( m >= x & S2[m] implies S2[m + 1] ) assume that A24: m >= x and A25: S2[m] ; ::_thesis: S2[m + 1] reconsider m1 = m as Element of NAT by ORDINAL1:def_12; assume that x <= m + 1 and A26: m + 1 < len rF ; ::_thesis: f . (m + 1) >= r m + 1 in dom rF by A26, NAT_1:44; then A27: rF . (m + 1) in rng rF by FUNCT_1:def_3; f . (m1 + 1) = addreal . ((f . m1),(rF . (m1 + 1))) by A11, A26; then ( f . (m1 + 1) = (f . m1) + (rF . (m1 + 1)) & rF . (m1 + 1) >= 0 ) by A27, A1, BINOP_2:def_9, PARTFUN3:def_4; then f . (m + 1) >= r + 0 by A24, A25, A26, NAT_1:13, XREAL_1:7; hence f . (m + 1) >= r ; ::_thesis: verum end; for m being Nat st m >= x holds S2[m] from NAT_1:sch_8(A22, A23); then addreal "**" rF >= r by A12, A9, A7; hence Sum rF >= r by Th48; ::_thesis: verum end; theorem Th62: :: AFINSQ_2:62 for rF being real-valued XFinSequence st rF is nonnegative-yielding holds ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) ) proof let rF be real-valued XFinSequence; ::_thesis: ( rF is nonnegative-yielding implies ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) ) ) assume A1: rF is nonnegative-yielding ; ::_thesis: ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) ) hereby ::_thesis: ( ( len rF = 0 or rF = (len rF) --> 0 ) implies Sum rF = 0 ) assume A2: Sum rF = 0 ; ::_thesis: ( len rF <> 0 implies not rF <> (len rF) --> 0 ) assume len rF <> 0 ; ::_thesis: not rF <> (len rF) --> 0 set L = (len rF) --> 0; assume rF <> (len rF) --> 0 ; ::_thesis: contradiction then consider k being Nat such that A3: ( k in dom ((len rF) --> 0) & ((len rF) --> 0) . k <> rF . k ) by AFINSQ_1:8, FUNCOP_1:13; rF . k in rng rF by A3, FUNCT_1:def_3; then ( ((len rF) --> 0) . k = 0 & rF . k >= 0 ) by A3, A1, FUNCOP_1:7, PARTFUN3:def_4; hence contradiction by A2, Th61, A1, A3; ::_thesis: verum end; A4: rF is COMPLEX -valued by Lm3; assume ( len rF = 0 or rF = (len rF) --> 0 ) ; ::_thesis: Sum rF = 0 then ( Sum rF = 0 or Sum rF = (len rF) * 0 ) by A4, Th58, Def8, BINOP_2:1; hence Sum rF = 0 ; ::_thesis: verum end; theorem Th63: :: AFINSQ_2:63 for n being Nat for cF being complex-valued XFinSequence for c being complex number holds c (#) (cF | n) = (c (#) cF) | n proof let n be Nat; ::_thesis: for cF being complex-valued XFinSequence for c being complex number holds c (#) (cF | n) = (c (#) cF) | n let cF be complex-valued XFinSequence; ::_thesis: for c being complex number holds c (#) (cF | n) = (c (#) cF) | n let c be complex number ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n set ccF = c (#) cF; set cFn = cF | n; A1: ( len (c (#) cF) = len cF & len (c (#) (cF | n)) = len (cF | n) ) by VALUED_1:def_5; percases ( n <= len cF or n > len cF ) ; supposeA2: n <= len cF ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n then A3: ( len (cF | n) = n & len ((c (#) cF) | n) = n ) by A1, AFINSQ_1:54; now__::_thesis:_for_i_being_Nat_st_i_<_len_(c_(#)_(cF_|_n))_holds_ (c_(#)_(cF_|_n))_._i_=_((c_(#)_cF)_|_n)_._i let i be Nat; ::_thesis: ( i < len (c (#) (cF | n)) implies (c (#) (cF | n)) . i = ((c (#) cF) | n) . i ) assume i < len (c (#) (cF | n)) ; ::_thesis: (c (#) (cF | n)) . i = ((c (#) cF) | n) . i then A4: i in dom (c (#) (cF | n)) by NAT_1:44; thus (c (#) (cF | n)) . i = c * ((cF | n) . i) by VALUED_1:6 .= c * (cF . i) by A4, A2, AFINSQ_1:53 .= (c (#) cF) . i by VALUED_1:6 .= ((c (#) cF) | n) . i by A4, A1, A2, AFINSQ_1:53 ; ::_thesis: verum end; hence c (#) (cF | n) = (c (#) cF) | n by A1, A3, AFINSQ_1:9; ::_thesis: verum end; suppose n > len cF ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n then ( cF | n = cF & (c (#) cF) | n = c (#) cF ) by A1, AFINSQ_1:52; hence c (#) (cF | n) = (c (#) cF) | n ; ::_thesis: verum end; end; end; theorem :: AFINSQ_2:64 for cF being complex-valued XFinSequence for c being complex number holds c * (Sum cF) = Sum (c (#) cF) proof let cF be complex-valued XFinSequence; ::_thesis: for c being complex number holds c * (Sum cF) = Sum (c (#) cF) let c be complex number ; ::_thesis: c * (Sum cF) = Sum (c (#) cF) defpred S1[ Nat] means for cF being complex-valued XFinSequence st dom cF = $1 holds c * (Sum cF) = Sum (c (#) cF); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] A3: k < k + 1 by NAT_1:13; let cF be complex-valued XFinSequence; ::_thesis: ( dom cF = k + 1 implies c * (Sum cF) = Sum (c (#) cF) ) assume A4: dom cF = k + 1 ; ::_thesis: c * (Sum cF) = Sum (c (#) cF) set cF1 = c (#) cF; A5: dom cF = dom (c (#) cF) by VALUED_1:def_5; reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3; A6: cF | (k + 1) = cF by A4, RELAT_1:69; len cF = k + 1 by A4; then A7: len (cF | k) = k by A3, AFINSQ_1:11; k < k + 1 by NAT_1:13; then A8: k in dom cF by A4, NAT_1:44; then addcomplex . ((addcomplex "**" (cF | k)),(cF . k)) = addcomplex "**" (cF | (k + 1)) by Th43; then A9: Sum cF = (Sum (cF | k)) + (cF . k) by A6, BINOP_2:def_3; A10: c * (Sum (cF | k)) = Sum (c (#) (cF | k)) by A2, A7 .= Sum (cF1 | k) by Th63 ; A11: c * (cF . k) = cF1 . k by VALUED_1:6; A12: cF1 | (k + 1) = cF1 by A4, A5, RELAT_1:69; addcomplex . ((addcomplex "**" (cF1 | k)),(cF1 . k)) = addcomplex "**" (cF1 | (k + 1)) by A5, A8, Th43; then Sum cF1 = (Sum (cF1 | k)) + (cF1 . k) by A12, BINOP_2:def_3; hence c * (Sum cF) = Sum (c (#) cF) by A9, A11, A10; ::_thesis: verum end; A13: S1[ 0 ] proof let cF be complex-valued XFinSequence; ::_thesis: ( dom cF = 0 implies c * (Sum cF) = Sum (c (#) cF) ) assume A14: dom cF = 0 ; ::_thesis: c * (Sum cF) = Sum (c (#) cF) set cF1 = c (#) cF; reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3; len cF = 0 by A14; then A15: addcomplex "**" cF = 0 by Def8, BINOP_2:1; len cF1 = 0 by A14, VALUED_1:def_5; hence c * (Sum cF) = Sum (c (#) cF) by A15, Def8, BINOP_2:1; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A1); then S1[ len cF] ; hence c * (Sum cF) = Sum (c (#) cF) ; ::_thesis: verum end; theorem Th65: :: AFINSQ_2:65 for n being Nat for cF being complex-valued XFinSequence st n in dom cF holds (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) proof let n be Nat; ::_thesis: for cF being complex-valued XFinSequence st n in dom cF holds (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) let cF be complex-valued XFinSequence; ::_thesis: ( n in dom cF implies (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) ) assume A1: n in dom cF ; ::_thesis: (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) reconsider cF = cF as XFinSequence of COMPLEX by Lm3; addcomplex . ((addcomplex "**" (cF | n)),(cF . n)) = addcomplex "**" (cF | (n + 1)) by Th43, A1; hence (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) by BINOP_2:def_3; ::_thesis: verum end; theorem Th66: :: AFINSQ_2:66 for y, x being set for f being Function st f . y = x & y in dom f holds {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} proof let y, x be set ; ::_thesis: for f being Function st f . y = x & y in dom f holds {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} let f be Function; ::_thesis: ( f . y = x & y in dom f implies {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} ) assume that A1: f . y = x and A2: y in dom f ; ::_thesis: {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} set d = (dom f) \ {y}; A3: (f | ((dom f) \ {y})) " {x} c= f " {x} proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} ) assume A4: x1 in (f | ((dom f) \ {y})) " {x} ; ::_thesis: x1 in f " {x} A5: (f | ((dom f) \ {y})) . x1 in {x} by A4, FUNCT_1:def_7; A6: x1 in dom (f | ((dom f) \ {y})) by A4, FUNCT_1:def_7; then ( dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) & f . x1 = (f | ((dom f) \ {y})) . x1 ) by FUNCT_1:47, RELAT_1:61; hence x1 in f " {x} by A6, A5, FUNCT_1:def_7; ::_thesis: verum end; A7: f " {x} c= {y} \/ ((f | ((dom f) \ {y})) " {x}) proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in f " {x} or x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) ) assume A8: x1 in f " {x} ; ::_thesis: x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) ( ( x1 in dom f & not x1 in {y} ) or x1 = y ) by A8, FUNCT_1:def_7, TARSKI:def_1; then ( ( x1 in dom f & x1 in (dom f) \ {y} & dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) ) or x1 = y ) by RELAT_1:61, XBOOLE_0:def_5; then ( x1 in dom (f | ((dom f) \ {y})) or x1 = y ) by XBOOLE_0:def_4; then ( ( x1 in dom (f | ((dom f) \ {y})) & f . x1 = (f | ((dom f) \ {y})) . x1 & f . x1 in {x} ) or x1 in {y} ) by A8, FUNCT_1:47, FUNCT_1:def_7, TARSKI:def_1; then ( x1 in (f | ((dom f) \ {y})) " {x} or x1 in {y} ) by FUNCT_1:def_7; hence x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) by XBOOLE_0:def_3; ::_thesis: verum end; {y} c= f " {x} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {y} or z in f " {x} ) assume z in {y} ; ::_thesis: z in f " {x} then A9: z = y by TARSKI:def_1; f . y in {x} by A1, TARSKI:def_1; hence z in f " {x} by A2, A9, FUNCT_1:def_7; ::_thesis: verum end; then {y} \/ ((f | ((dom f) \ {y})) " {x}) c= f " {x} by A3, XBOOLE_1:8; hence {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} by A7, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th67: :: AFINSQ_2:67 for y, x being set for f being Function st f . y <> x holds (f | ((dom f) \ {y})) " {x} = f " {x} proof let y, x be set ; ::_thesis: for f being Function st f . y <> x holds (f | ((dom f) \ {y})) " {x} = f " {x} let f be Function; ::_thesis: ( f . y <> x implies (f | ((dom f) \ {y})) " {x} = f " {x} ) set d = (dom f) \ {y}; assume A1: f . y <> x ; ::_thesis: (f | ((dom f) \ {y})) " {x} = f " {x} A2: f " {x} c= (f | ((dom f) \ {y})) " {x} proof A3: dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) by RELAT_1:61; let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in f " {x} or x1 in (f | ((dom f) \ {y})) " {x} ) assume A4: x1 in f " {x} ; ::_thesis: x1 in (f | ((dom f) \ {y})) " {x} A5: f . x1 in {x} by A4, FUNCT_1:def_7; f . x1 in {x} by A4, FUNCT_1:def_7; then f . x1 = x by TARSKI:def_1; then A6: not x1 in {y} by A1, TARSKI:def_1; x1 in dom f by A4, FUNCT_1:def_7; then x1 in (dom f) \ {y} by A6, XBOOLE_0:def_5; then A7: x1 in dom (f | ((dom f) \ {y})) by A3, XBOOLE_0:def_4; then f . x1 = (f | ((dom f) \ {y})) . x1 by FUNCT_1:47; hence x1 in (f | ((dom f) \ {y})) " {x} by A7, A5, FUNCT_1:def_7; ::_thesis: verum end; (f | ((dom f) \ {y})) " {x} c= f " {x} proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} ) assume A8: x1 in (f | ((dom f) \ {y})) " {x} ; ::_thesis: x1 in f " {x} A9: (f | ((dom f) \ {y})) . x1 in {x} by A8, FUNCT_1:def_7; A10: x1 in dom (f | ((dom f) \ {y})) by A8, FUNCT_1:def_7; then ( dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) & f . x1 = (f | ((dom f) \ {y})) . x1 ) by FUNCT_1:47, RELAT_1:61; hence x1 in f " {x} by A10, A9, FUNCT_1:def_7; ::_thesis: verum end; hence (f | ((dom f) \ {y})) " {x} = f " {x} by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: AFINSQ_2:68 for cF being complex-valued XFinSequence for c being complex number st rng cF c= {0,c} holds Sum cF = c * (card (cF " {c})) proof let cF be complex-valued XFinSequence; ::_thesis: for c being complex number st rng cF c= {0,c} holds Sum cF = c * (card (cF " {c})) let c be complex number ; ::_thesis: ( rng cF c= {0,c} implies Sum cF = c * (card (cF " {c})) ) defpred S1[ Nat] means for cF being complex-valued XFinSequence for c being complex number st dom cF = $1 & rng cF c= {0,c} holds Sum cF = c * (card (cF " {c})); assume A1: rng cF c= {0,c} ; ::_thesis: Sum cF = c * (card (cF " {c})) A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] let F be complex-valued XFinSequence; ::_thesis: for c being complex number st dom F = k + 1 & rng F c= {0,c} holds Sum F = c * (card (F " {c})) let c be complex number ; ::_thesis: ( dom F = k + 1 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) ) assume that A4: dom F = k + 1 and A5: rng F c= {0,c} ; ::_thesis: Sum F = c * (card (F " {c})) percases ( c <> 0 or c = 0 ) ; supposeA6: c <> 0 ; ::_thesis: Sum F = c * (card (F " {c})) ( not k in k & k \/ {k} = k + 1 ) by AFINSQ_1:2; then A7: (dom F) \ {k} = k by A4, ZFMISC_1:117; k < k + 1 by NAT_1:13; then k in dom F by A4, NAT_1:44; then A8: F . k in rng F by FUNCT_1:def_3; percases ( F . k = 0 or F . k = c ) by A5, A8, TARSKI:def_2; supposeA9: F . k = 0 ; ::_thesis: Sum F = c * (card (F " {c})) A10: F | (k + 1) = F by A4, RELAT_1:69; A11: k < k + 1 by NAT_1:13; then k in dom F by A4, NAT_1:44; then A12: (Sum (F | k)) + 0 = Sum F by A9, A10, Th65; dom F = len F ; then A13: len (F | k) = k by A4, A11, AFINSQ_1:54; ( rng (F | k) c= rng F & (F | k) " {c} = F " {c} ) by A6, A7, A9, Th67; hence Sum F = c * (card (F " {c})) by A3, A5, A13, A12, XBOOLE_1:1; ::_thesis: verum end; supposeA14: F . k = c ; ::_thesis: Sum F = c * (card (F " {c})) set Fk = (F | k) " {c}; not k in k ; then not k in dom (F | k) ; then A15: not k in (F | k) " {c} by FUNCT_1:def_7; A16: k < k + 1 by NAT_1:13; then A17: k in dom F by A4, NAT_1:44; dom F = len F ; then ( rng (F | k) c= rng F & len (F | k) = k ) by A4, A16, AFINSQ_1:54; then A18: Sum (F | k) = c * (card ((F | k) " {c})) by A3, A5, XBOOLE_1:1; F | (k + 1) = F by A4, RELAT_1:69; then A19: (Sum (F | k)) + c = Sum F by A14, A17, Th65; {k} \/ ((F | k) " {c}) = F " {c} by A7, A14, A17, Th66; then (card ((F | k) " {c})) + 1 = card (F " {c}) by A15, CARD_2:41; hence Sum F = c * (card (F " {c})) by A18, A19; ::_thesis: verum end; end; end; supposeA20: c = 0 ; ::_thesis: Sum F = c * (card (F " {c})) for x being set st x in dom F holds F . x = 0 proof let x be set ; ::_thesis: ( x in dom F implies F . x = 0 ) assume x in dom F ; ::_thesis: F . x = 0 then F . x in rng F by FUNCT_1:def_3; hence F . x = 0 by A5, A20, TARSKI:def_2; ::_thesis: verum end; then F = (dom F) --> 0 by FUNCOP_1:11; then Sum F = (len F) * 0 by Th62; hence Sum F = c * (card (F " {c})) by A20; ::_thesis: verum end; end; end; A21: S1[ 0 ] proof let F be complex-valued XFinSequence; ::_thesis: for c being complex number st dom F = 0 & rng F c= {0,c} holds Sum F = c * (card (F " {c})) let c be complex number ; ::_thesis: ( dom F = 0 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) ) assume that A22: dom F = 0 and rng F c= {0,c} ; ::_thesis: Sum F = c * (card (F " {c})) ( F " {c} c= 0 & F = {} ) by A22, RELAT_1:132; then ( card (F " {c}) = 0 & Sum F = 0 ) ; hence Sum F = c * (card (F " {c})) ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A21, A2); then S1[ len cF] ; hence Sum cF = c * (card (cF " {c})) by A1; ::_thesis: verum end; theorem :: AFINSQ_2:69 for cF being complex-valued XFinSequence holds Sum cF = Sum (Rev cF) proof let cF be complex-valued XFinSequence; ::_thesis: Sum cF = Sum (Rev cF) cF is COMPLEX -valued by Lm3; then reconsider Fr2 = cF, Fr1 = Rev cF as XFinSequence of COMPLEX ; A1: len Fr1 = len Fr2 by Def1; defpred S1[ set , set ] means for i being Nat st i = $1 holds $2 = (len Fr1) - (1 + i); A2: card (len Fr1) = card (len Fr1) ; A3: for x being set st x in len Fr1 holds ex y being set st ( y in len Fr1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in len Fr1 implies ex y being set st ( y in len Fr1 & S1[x,y] ) ) assume A4: x in len Fr1 ; ::_thesis: ex y being set st ( y in len Fr1 & S1[x,y] ) reconsider k = x as Element of NAT by Th1, A4; k < len Fr1 by A4, NAT_1:44; then k + 1 <= len Fr1 by NAT_1:13; then A5: (len Fr1) -' (1 + k) = (len Fr1) - (1 + k) by XREAL_1:233; take (len Fr1) -' (1 + k) ; ::_thesis: ( (len Fr1) -' (1 + k) in len Fr1 & S1[x,(len Fr1) -' (1 + k)] ) (len Fr1) + 0 < (len Fr1) + (1 + k) by XREAL_1:8; then (len Fr1) - (1 + k) < ((len Fr1) + (1 + k)) - (1 + k) by XREAL_1:9; hence ( (len Fr1) -' (1 + k) in len Fr1 & S1[x,(len Fr1) -' (1 + k)] ) by A5, NAT_1:44; ::_thesis: verum end; consider P being Function of (len Fr1),(len Fr1) such that A6: for x being set st x in len Fr1 holds S1[x,P . x] from FUNCT_2:sch_1(A3); A7: for x1, x2 being set st x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 implies x1 = x2 ) assume that A8: x1 in len Fr1 and A9: x2 in len Fr1 and A10: P . x1 = P . x2 ; ::_thesis: x1 = x2 reconsider i = x1, j = x2 as Element of NAT by A8, A9, Th1; A11: P . x2 = (len Fr1) - (1 + j) by A6, A9; P . x1 = (len Fr1) - (1 + i) by A6, A8; hence x1 = x2 by A10, A11; ::_thesis: verum end; then A12: P is one-to-one by FUNCT_2:56; P is one-to-one by A7, FUNCT_2:56; then P is onto by A2, Lm2; then reconsider P = P as Permutation of (dom Fr1) by A12; A13: now__::_thesis:_for_x_being_set_st_x_in_dom_Fr1_holds_ Fr1_._x_=_Fr2_._(P_._x) let x be set ; ::_thesis: ( x in dom Fr1 implies Fr1 . x = Fr2 . (P . x) ) assume A14: x in dom Fr1 ; ::_thesis: Fr1 . x = Fr2 . (P . x) reconsider k = x as Element of NAT by A14; P . k = (len Fr1) - (1 + k) by A6, A14; hence Fr1 . x = Fr2 . (P . x) by A1, Def1, A14; ::_thesis: verum end; A15: now__::_thesis:_for_x_being_set_st_x_in_dom_Fr1_holds_ (_x_in_dom_P_&_P_._x_in_dom_Fr2_) let x be set ; ::_thesis: ( x in dom Fr1 implies ( x in dom P & P . x in dom Fr2 ) ) assume A16: x in dom Fr1 ; ::_thesis: ( x in dom P & P . x in dom Fr2 ) x in dom P by A16, FUNCT_2:52; then P . x in rng P by FUNCT_1:3; hence ( x in dom P & P . x in dom Fr2 ) by A1, A16, FUNCT_2:52; ::_thesis: verum end; for x being set st x in dom P & P . x in dom Fr2 holds x in dom Fr1 ; then Fr1 = Fr2 * P by A15, A13, FUNCT_1:10; hence Sum cF = Sum (Rev cF) by A1, Th45; ::_thesis: verum end; theorem Th70: :: AFINSQ_2:70 for f being Function for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds fp ^ fq = f * (p ^ q) proof let f be Function; ::_thesis: for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds fp ^ fq = f * (p ^ q) let p, q, fp, fq be XFinSequence; ::_thesis: ( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q implies fp ^ fq = f * (p ^ q) ) assume A1: ( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q ) ; ::_thesis: fp ^ fq = f * (p ^ q) set pq = p ^ q; A2: rng (p ^ q) = (rng p) \/ (rng q) by AFINSQ_1:26; then A3: dom (f * (p ^ q)) = dom (p ^ q) by A1, RELAT_1:27, XBOOLE_1:8; reconsider fpq = f * (p ^ q) as XFinSequence by A2, A1, AFINSQ_1:10, XBOOLE_1:8; A4: ( dom fp = dom p & dom fq = dom q ) by A1, RELAT_1:27; A5: ( dom (p ^ q) = (len p) + (len q) & dom (fp ^ fq) = (len fp) + (len fq) ) by AFINSQ_1:def_3; A6: len fpq = len (fp ^ fq) by A2, A1, A4, A5, RELAT_1:27, XBOOLE_1:8; for k being Nat st k < len fpq holds (fp ^ fq) . k = fpq . k proof let k be Nat; ::_thesis: ( k < len fpq implies (fp ^ fq) . k = fpq . k ) assume A7: k < len fpq ; ::_thesis: (fp ^ fq) . k = fpq . k then A8: k in dom fpq by NAT_1:44; percases ( k < len p or k >= len p ) ; suppose k < len p ; ::_thesis: (fp ^ fq) . k = fpq . k then k in dom p by NAT_1:44; then ( (p ^ q) . k = p . k & fp . k = f . (p . k) & (fp ^ fq) . k = fp . k ) by A1, A4, AFINSQ_1:def_3, FUNCT_1:13; hence (fp ^ fq) . k = fpq . k by A8, FUNCT_1:12; ::_thesis: verum end; supposeA9: k >= len p ; ::_thesis: (fp ^ fq) . k = fpq . k then reconsider kp = k - (len p) as Element of NAT by NAT_1:21; (len p) + kp < (len p) + (len q) by A5, A2, A1, A7, RELAT_1:27, XBOOLE_1:8; then kp < len q by XREAL_1:7; then kp in dom q by NAT_1:44; then ( (p ^ q) . k = q . kp & (fp ^ fq) . k = fq . kp & fq . kp = f . (q . kp) ) by A7, A1, A3, A4, A5, A9, AFINSQ_1:18, FUNCT_1:13; hence (fp ^ fq) . k = fpq . k by A8, FUNCT_1:12; ::_thesis: verum end; end; end; hence fp ^ fq = f * (p ^ q) by A6, AFINSQ_1:9; ::_thesis: verum end; theorem :: AFINSQ_2:71 for cF being complex-valued XFinSequence for B1, B2 being finite natural-membered set st B1 D) = the_unity_wrt b proof let D be non empty set ; ::_thesis: for b being BinOp of D st b is having_a_unity holds b "**" (<%> D) = the_unity_wrt b let b be BinOp of D; ::_thesis: ( b is having_a_unity implies b "**" (<%> D) = the_unity_wrt b ) A1: len (<%> D) = 0 ; assume b is having_a_unity ; ::_thesis: b "**" (<%> D) = the_unity_wrt b hence b "**" (<%> D) = the_unity_wrt b by A1, Def8; ::_thesis: verum end; definition let D be set ; let F be XFinSequence of D ^omega ; func FlattenSeq F -> Element of D ^omega means :Def10: :: AFINSQ_2:def 10 ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it = g "**" F ); existence ex b1 being Element of D ^omega ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F ) proof deffunc H1( Element of D ^omega , Element of D ^omega ) -> Element of D ^omega = $1 ^ $2; consider g being BinOp of (D ^omega) such that A1: for a, b being Element of D ^omega holds g . (a,b) = H1(a,b) from BINOP_1:sch_4(); take g "**" F ; ::_thesis: ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) take g ; ::_thesis: ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) thus ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of D ^omega st ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F ) & ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b2 = g "**" F ) holds b1 = b2 proof let it1, it2 be Element of D ^omega ; ::_thesis: ( ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it1 = g "**" F ) & ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it2 = g "**" F ) implies it1 = it2 ) given g1 being BinOp of (D ^omega) such that A2: for p, q being Element of D ^omega holds g1 . (p,q) = p ^ q and A3: it1 = g1 "**" F ; ::_thesis: ( for g being BinOp of (D ^omega) holds ( ex p, q being Element of D ^omega st not g . (p,q) = p ^ q or not it2 = g "**" F ) or it1 = it2 ) given g2 being BinOp of (D ^omega) such that A4: for p, q being Element of D ^omega holds g2 . (p,q) = p ^ q and A5: it2 = g2 "**" F ; ::_thesis: it1 = it2 now__::_thesis:_for_a,_b_being_Element_of_D_^omega_holds_g1_._(a,b)_=_g2_._(a,b) let a, b be Element of D ^omega ; ::_thesis: g1 . (a,b) = g2 . (a,b) thus g1 . (a,b) = a ^ b by A2 .= g2 . (a,b) by A4 ; ::_thesis: verum end; hence it1 = it2 by A3, A5, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines FlattenSeq AFINSQ_2:def_10_:_ for D being set for F being XFinSequence of D ^omega for b3 being Element of D ^omega holds ( b3 = FlattenSeq F iff ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b3 = g "**" F ) ); theorem :: AFINSQ_2:73 for D being set for d being Element of D ^omega holds FlattenSeq <%d%> = d proof let D be set ; ::_thesis: for d being Element of D ^omega holds FlattenSeq <%d%> = d let d be Element of D ^omega ; ::_thesis: FlattenSeq <%d%> = d ex g being BinOp of (D ^omega) st ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & FlattenSeq <%d%> = g "**" <%d%> ) by Def10; hence FlattenSeq <%d%> = d by Th37; ::_thesis: verum end; theorem :: AFINSQ_2:74 for D being set holds FlattenSeq (<%> (D ^omega)) = <%> D proof let D be set ; ::_thesis: FlattenSeq (<%> (D ^omega)) = <%> D consider g being BinOp of (D ^omega) such that A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq (<%> (D ^omega)) = g "**" (<%> (D ^omega)) by Def10; A3: {} is Element of D ^omega by AFINSQ_1:43; reconsider p = {} as Element of D ^omega by AFINSQ_1:43; now__::_thesis:_for_a_being_Element_of_D_^omega_holds_ (_g_._({},a)_=_a_&_g_._(a,{})_=_a_) let a be Element of D ^omega ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a ) thus g . ({},a) = {} ^ a by A1, A3 .= a ; ::_thesis: g . (a,{}) = a thus g . (a,{}) = a ^ {} by A1, A3 .= a ; ::_thesis: verum end; then A4: p is_a_unity_wrt g by BINOP_1:3; then g is having_a_unity by SETWISEO:def_2; then g "**" (<%> (D ^omega)) = the_unity_wrt g by Th72; hence FlattenSeq (<%> (D ^omega)) = <%> D by A2, A4, BINOP_1:def_8; ::_thesis: verum end; theorem Th75: :: AFINSQ_2:75 for D being set for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) proof let D be set ; ::_thesis: for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) let F, G be XFinSequence of D ^omega ; ::_thesis: FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) consider g being BinOp of (D ^omega) such that A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq (F ^ G) = g "**" (F ^ G) by Def10; now__::_thesis:_for_a,_b,_c_being_Element_of_D_^omega_holds_g_._(a,(g_._(b,c)))_=_g_._((g_._(a,b)),c) let a, b, c be Element of D ^omega ; ::_thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c) thus g . (a,(g . (b,c))) = a ^ (g . (b,c)) by A1 .= a ^ (b ^ c) by A1 .= (a ^ b) ^ c by AFINSQ_1:27 .= (g . (a,b)) ^ c by A1 .= g . ((g . (a,b)),c) by A1 ; ::_thesis: verum end; then A3: g is associative by BINOP_1:def_3; A4: {} is Element of D ^omega by AFINSQ_1:43; reconsider p = {} as Element of D ^omega by AFINSQ_1:43; now__::_thesis:_for_a_being_Element_of_D_^omega_holds_ (_g_._({},a)_=_a_&_g_._(a,{})_=_a_) let a be Element of D ^omega ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a ) thus g . ({},a) = {} ^ a by A1, A4 .= a ; ::_thesis: g . (a,{}) = a thus g . (a,{}) = a ^ {} by A1, A4 .= a ; ::_thesis: verum end; then p is_a_unity_wrt g by BINOP_1:3; then ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) by SETWISEO:def_2; hence FlattenSeq (F ^ G) = g . ((g "**" F),(g "**" G)) by A2, A3, Th41 .= (g "**" F) ^ (g "**" G) by A1 .= (FlattenSeq F) ^ (g "**" G) by A1, Def10 .= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def10 ; ::_thesis: verum end; theorem :: AFINSQ_2:76 for D being set for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q proof let D be set ; ::_thesis: for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q let p, q be Element of D ^omega ; ::_thesis: FlattenSeq <%p,q%> = p ^ q consider g being BinOp of (D ^omega) such that A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq <%p,q%> = g "**" <%p,q%> by Def10; thus FlattenSeq <%p,q%> = g . (p,q) by A2, Th38 .= p ^ q by A1 ; ::_thesis: verum end; theorem :: AFINSQ_2:77 for D being set for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r proof let D be set ; ::_thesis: for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r let p, q, r be Element of D ^omega ; ::_thesis: FlattenSeq <%p,q,r%> = (p ^ q) ^ r consider g being BinOp of (D ^omega) such that A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq <%p,q,r%> = g "**" <%p,q,r%> by Def10; thus FlattenSeq <%p,q,r%> = g . ((g . (p,q)),r) by A2, Th39 .= (g . (p,q)) ^ r by A1 .= (p ^ q) ^ r by A1 ; ::_thesis: verum end; theorem Th78: :: AFINSQ_2:78 for p, q being XFinSequence st p c= q holds p ^ (q /^ (len p)) = q proof let p, q be XFinSequence; ::_thesis: ( p c= q implies p ^ (q /^ (len p)) = q ) assume A1: p c= q ; ::_thesis: p ^ (q /^ (len p)) = q A2: (len p) + (len (q /^ (len p))) = (len p) + ((len q) -' (len p)) by Def2 .= ((len q) + (len p)) -' (len p) by A1, NAT_1:43, NAT_D:38 .= dom q by NAT_D:34 ; A3: for k being Nat st k in dom p holds q . k = p . k by A1, GRFUNC_1:2; for k being Nat st k in dom (q /^ (len p)) holds q . ((len p) + k) = (q /^ (len p)) . k by Def2; hence p ^ (q /^ (len p)) = q by A2, A3, AFINSQ_1:def_3; ::_thesis: verum end; theorem Th79: :: AFINSQ_2:79 for p, q being XFinSequence st p c= q holds ex r being XFinSequence st p ^ r = q proof let p, q be XFinSequence; ::_thesis: ( p c= q implies ex r being XFinSequence st p ^ r = q ) assume A1: p c= q ; ::_thesis: ex r being XFinSequence st p ^ r = q take r = q /^ (len p); ::_thesis: p ^ r = q thus p ^ r = q by A1, Th78; ::_thesis: verum end; theorem Th80: :: AFINSQ_2:80 for D being non empty set for p, q being XFinSequence of D st p c= q holds ex r being XFinSequence of D st p ^ r = q proof let D be non empty set ; ::_thesis: for p, q being XFinSequence of D st p c= q holds ex r being XFinSequence of D st p ^ r = q let p, q be XFinSequence of D; ::_thesis: ( p c= q implies ex r being XFinSequence of D st p ^ r = q ) assume p c= q ; ::_thesis: ex r being XFinSequence of D st p ^ r = q then consider r being XFinSequence such that A1: p ^ r = q by Th79; reconsider r = r as XFinSequence of D by A1, AFINSQ_1:31; take r ; ::_thesis: p ^ r = q thus p ^ r = q by A1; ::_thesis: verum end; theorem :: AFINSQ_2:81 for q, p, r being XFinSequence st q c= r holds p ^ q c= p ^ r proof let q, p, r be XFinSequence; ::_thesis: ( q c= r implies p ^ q c= p ^ r ) assume q c= r ; ::_thesis: p ^ q c= p ^ r then consider s being XFinSequence such that A1: q ^ s = r by Th79; p ^ q c= (p ^ q) ^ s by AFINSQ_1:74; hence p ^ q c= p ^ r by A1, AFINSQ_1:27; ::_thesis: verum end; theorem :: AFINSQ_2:82 for D being set for F, G being XFinSequence of D ^omega st F c= G holds FlattenSeq F c= FlattenSeq G proof let D be set ; ::_thesis: for F, G being XFinSequence of D ^omega st F c= G holds FlattenSeq F c= FlattenSeq G let F, G be XFinSequence of D ^omega ; ::_thesis: ( F c= G implies FlattenSeq F c= FlattenSeq G ) assume F c= G ; ::_thesis: FlattenSeq F c= FlattenSeq G then consider F9 being XFinSequence of D ^omega such that A1: F ^ F9 = G by Th80; (FlattenSeq F) ^ (FlattenSeq F9) = FlattenSeq G by A1, Th75; hence FlattenSeq F c= FlattenSeq G by AFINSQ_1:74; ::_thesis: verum end; registration let p be XFinSequence; let q be non empty XFinSequence; clusterp ^ q -> non empty ; coherence not p ^ q is empty by AFINSQ_1:30; clusterq ^ p -> non empty ; coherence not q ^ p is empty by AFINSQ_1:30; end; theorem :: AFINSQ_2:83 for x being set for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p proof let x be set ; ::_thesis: for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p let p be XFinSequence; ::_thesis: CutLastLoc (p ^ <%x%>) = p set q = CutLastLoc (p ^ <%x%>); A1: (len (p ^ <%x%>)) -' 1 = ((len p) + 1) -' 1 by AFINSQ_1:75 .= len p by NAT_D:34 ; A2: dom (p ^ <%x%>) = len (p ^ <%x%>) .= (len p) + 1 by AFINSQ_1:75 .= (dom p) \/ {(len p)} by AFINSQ_1:2 ; A3: not len p in dom p ; LastLoc (p ^ <%x%>) = (len (p ^ <%x%>)) -' 1 by AFINSQ_1:70; hence A4: dom (CutLastLoc (p ^ <%x%>)) = (dom (p ^ <%x%>)) \ {(len p)} by A1, VALUED_1:36 .= dom p by A2, A3, ZFMISC_1:117 ; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . b1 = p . b1 ) let y be set ; ::_thesis: ( not y in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . y = p . y ) assume A5: y in dom (CutLastLoc (p ^ <%x%>)) ; ::_thesis: (CutLastLoc (p ^ <%x%>)) . y = p . y A6: p c= p ^ <%x%> by AFINSQ_1:74; thus (CutLastLoc (p ^ <%x%>)) . y = (p ^ <%x%>) . y by A5, GRFUNC_1:2 .= p . y by A5, A4, A6, GRFUNC_1:2 ; ::_thesis: verum end;