:: RFINSEQ semantic presentation begin registration let f be FinSequence; let x be set ; cluster Coim (f,x) -> finite ; coherence Coim (f,x) is finite ; end; theorem Th1: :: RFINSEQ:1 for f, g, h being FinSequence holds ( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent ) proof let f, g, h be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent ) thus ( f,g are_fiberwise_equipotent implies f ^ h,g ^ h are_fiberwise_equipotent ) ::_thesis: ( f ^ h,g ^ h are_fiberwise_equipotent implies f,g are_fiberwise_equipotent ) proof assume A1: f,g are_fiberwise_equipotent ; ::_thesis: f ^ h,g ^ h are_fiberwise_equipotent now__::_thesis:_for_y_being_set_holds_card_(Coim_((f_^_h),y))_=_card_(Coim_((g_^_h),y)) let y be set ; ::_thesis: card (Coim ((f ^ h),y)) = card (Coim ((g ^ h),y)) card (Coim (f,y)) = card (Coim (g,y)) by A1, CLASSES1:def_9; hence card (Coim ((f ^ h),y)) = (card (Coim (g,y))) + (card (Coim (h,y))) by FINSEQ_3:57 .= card (Coim ((g ^ h),y)) by FINSEQ_3:57 ; ::_thesis: verum end; hence f ^ h,g ^ h are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; assume A2: f ^ h,g ^ h are_fiberwise_equipotent ; ::_thesis: f,g are_fiberwise_equipotent now__::_thesis:_for_x_being_set_holds_card_(Coim_(f,x))_=_card_(Coim_(g,x)) let x be set ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x)) A3: ( card (Coim ((f ^ h),x)) = (card (Coim (f,x))) + (card (Coim (h,x))) & card (Coim ((g ^ h),x)) = (card (Coim (g,x))) + (card (Coim (h,x))) ) by FINSEQ_3:57; card (Coim ((f ^ h),x)) = card (Coim ((g ^ h),x)) by A2, CLASSES1:def_9; hence card (Coim (f,x)) = card (Coim (g,x)) by A3; ::_thesis: verum end; hence f,g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; theorem :: RFINSEQ:2 for f, g being FinSequence holds f ^ g,g ^ f are_fiberwise_equipotent proof let f, g be FinSequence; ::_thesis: f ^ g,g ^ f are_fiberwise_equipotent let y be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim ((f ^ g),y)) = card (Coim ((g ^ f),y)) thus card (Coim ((f ^ g),y)) = (card (g " {y})) + (card (f " {y})) by FINSEQ_3:57 .= card (Coim ((g ^ f),y)) by FINSEQ_3:57 ; ::_thesis: verum end; theorem Th3: :: RFINSEQ:3 for f, g being FinSequence st f,g are_fiberwise_equipotent holds ( len f = len g & dom f = dom g ) proof let f, g be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent implies ( len f = len g & dom f = dom g ) ) A1: dom f = Seg (len f) by FINSEQ_1:def_3; assume f,g are_fiberwise_equipotent ; ::_thesis: ( len f = len g & dom f = dom g ) then A2: ( card (f " (rng f)) = card (g " (rng f)) & rng f = rng g ) by CLASSES1:75, CLASSES1:78; A3: Seg (len g) = dom g by FINSEQ_1:def_3; thus len f = card (Seg (len f)) by FINSEQ_1:57 .= card (g " (rng g)) by A1, A2, RELAT_1:134 .= card (Seg (len g)) by A3, RELAT_1:134 .= len g by FINSEQ_1:57 ; ::_thesis: dom f = dom g hence dom f = dom g by A1, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th4: :: RFINSEQ:4 for f, g being FinSequence holds ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P ) proof let f, g be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P ) thus ( f,g are_fiberwise_equipotent implies ex P being Permutation of (dom g) st f = g * P ) ::_thesis: ( ex P being Permutation of (dom g) st f = g * P implies f,g are_fiberwise_equipotent ) proof assume A1: f,g are_fiberwise_equipotent ; ::_thesis: ex P being Permutation of (dom g) st f = g * P then dom f = dom g by Th3; hence ex P being Permutation of (dom g) st f = g * P by A1, CLASSES1:80; ::_thesis: verum end; given P being Permutation of (dom g) such that A2: f = g * P ; ::_thesis: f,g are_fiberwise_equipotent ( dom g = {} implies dom g = {} ) ; then ( rng P c= dom g & dom P = dom g ) by FUNCT_2:def_1, RELAT_1:def_19; then dom f = dom g by A2, RELAT_1:27; hence f,g are_fiberwise_equipotent by A2, CLASSES1:80; ::_thesis: verum end; defpred S1[ Nat] means for X being finite set for F being Function st card (dom (F | X)) = $1 holds ex a being FinSequence st F | X,a are_fiberwise_equipotent ; Lm1: S1[ 0 ] proof let X be finite set ; ::_thesis: for F being Function st card (dom (F | X)) = 0 holds ex a being FinSequence st F | X,a are_fiberwise_equipotent let F be Function; ::_thesis: ( card (dom (F | X)) = 0 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent ) assume A1: card (dom (F | X)) = 0 ; ::_thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent take A = {} ; ::_thesis: F | X,A are_fiberwise_equipotent let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim ((F | X),x)) = card (Coim (A,x)) dom (F | X) = {} by A1; hence card (Coim ((F | X),x)) = card (Coim (A,x)) by RELAT_1:132, XBOOLE_1:3; ::_thesis: verum end; Lm2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A1: S1[n] ; ::_thesis: S1[n + 1] let X be finite set ; ::_thesis: for F being Function st card (dom (F | X)) = n + 1 holds ex a being FinSequence st F | X,a are_fiberwise_equipotent let F be Function; ::_thesis: ( card (dom (F | X)) = n + 1 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent ) reconsider dx = dom (F | X) as finite set ; set x = the Element of dx; set Y = X \ { the Element of dx}; set dy = dom (F | (X \ { the Element of dx})); A2: dom (F | (X \ { the Element of dx})) = (dom F) /\ (X \ { the Element of dx}) by RELAT_1:61; A3: dx = (dom F) /\ X by RELAT_1:61; A4: dom (F | (X \ { the Element of dx})) = dx \ { the Element of dx} proof thus dom (F | (X \ { the Element of dx})) c= dx \ { the Element of dx} :: according to XBOOLE_0:def_10 ::_thesis: dx \ { the Element of dx} c= dom (F | (X \ { the Element of dx})) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (F | (X \ { the Element of dx})) or y in dx \ { the Element of dx} ) assume A5: y in dom (F | (X \ { the Element of dx})) ; ::_thesis: y in dx \ { the Element of dx} then y in X \ { the Element of dx} by A2, XBOOLE_0:def_4; then A6: not y in { the Element of dx} by XBOOLE_0:def_5; y in dom F by A2, A5, XBOOLE_0:def_4; then y in dx by A2, A3, A5, XBOOLE_0:def_4; hence y in dx \ { the Element of dx} by A6, XBOOLE_0:def_5; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dx \ { the Element of dx} or y in dom (F | (X \ { the Element of dx})) ) assume A7: y in dx \ { the Element of dx} ; ::_thesis: y in dom (F | (X \ { the Element of dx})) then ( not y in { the Element of dx} & y in X ) by A3, XBOOLE_0:def_4, XBOOLE_0:def_5; then A8: y in X \ { the Element of dx} by XBOOLE_0:def_5; y in dom F by A3, A7, XBOOLE_0:def_4; hence y in dom (F | (X \ { the Element of dx})) by A2, A8, XBOOLE_0:def_4; ::_thesis: verum end; assume A9: card (dom (F | X)) = n + 1 ; ::_thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent then { the Element of dx} c= dx by CARD_1:27, ZFMISC_1:31; then card (dom (F | (X \ { the Element of dx}))) = (card dx) - (card { the Element of dx}) by A4, CARD_2:44 .= (n + 1) - 1 by A9, CARD_1:30 .= n ; then consider a being FinSequence such that A10: F | (X \ { the Element of dx}),a are_fiberwise_equipotent by A1; take A = a ^ <*(F . the Element of dx)*>; ::_thesis: F | X,A are_fiberwise_equipotent dx <> {} by A9; then the Element of dx in dx ; then A11: the Element of dx in (dom F) /\ X by RELAT_1:61; then the Element of dx in dom F by XBOOLE_0:def_4; then A12: { the Element of dx} c= dom F by ZFMISC_1:31; the Element of dx in X by A11, XBOOLE_0:def_4; then A13: { the Element of dx} c= X by ZFMISC_1:31; now__::_thesis:_for_y_being_set_holds_card_(Coim_((F_|_X),y))_=_card_(Coim_(A,y)) let y be set ; ::_thesis: card (Coim ((F | X),y)) = card (Coim (A,y)) A14: X \ { the Element of dx} misses { the Element of dx} by XBOOLE_1:79; A15: ((F | (X \ { the Element of dx})) " {y}) \/ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) \/ ((F | { the Element of dx}) " {y}) by FUNCT_1:70 .= ((X \ { the Element of dx}) /\ (F " {y})) \/ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70 .= ((X \ { the Element of dx}) \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:23 .= (X \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:39 .= X /\ (F " {y}) by A13, XBOOLE_1:12 .= (F | X) " {y} by FUNCT_1:70 ; reconsider FF = <*(F . the Element of dx)*> " {y} as finite set ; A16: card (Coim ((F | (X \ { the Element of dx})),y)) = card (Coim (a,y)) by A10, CLASSES1:def_9; A17: dom (F | { the Element of dx}) = { the Element of dx} by A12, RELAT_1:62; A18: dom <*(F . the Element of dx)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; A19: now__::_thesis:_(_(_y_=_F_._the_Element_of_dx_&_card_((F_|_{_the_Element_of_dx})_"_{y})_=_card_FF_)_or_(_y_<>_F_._the_Element_of_dx_&_card_((F_|_{_the_Element_of_dx})_"_{y})_=_card_FF_)_) percases ( y = F . the Element of dx or y <> F . the Element of dx ) ; caseA20: y = F . the Element of dx ; ::_thesis: card ((F | { the Element of dx}) " {y}) = card FF A21: { the Element of dx} c= (F | { the Element of dx}) " {y} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { the Element of dx} or z in (F | { the Element of dx}) " {y} ) A22: y in {y} by TARSKI:def_1; assume A23: z in { the Element of dx} ; ::_thesis: z in (F | { the Element of dx}) " {y} then z = the Element of dx by TARSKI:def_1; then y = (F | { the Element of dx}) . z by A17, A20, A23, FUNCT_1:47; hence z in (F | { the Element of dx}) " {y} by A17, A23, A22, FUNCT_1:def_7; ::_thesis: verum end; (F | { the Element of dx}) " {y} c= { the Element of dx} by A17, RELAT_1:132; then (F | { the Element of dx}) " {y} = { the Element of dx} by A21, XBOOLE_0:def_10; then A24: card ((F | { the Element of dx}) " {y}) = 1 by CARD_1:30; A25: {1} c= <*(F . the Element of dx)*> " {y} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {1} or z in <*(F . the Element of dx)*> " {y} ) A26: y in {y} by TARSKI:def_1; assume A27: z in {1} ; ::_thesis: z in <*(F . the Element of dx)*> " {y} then z = 1 by TARSKI:def_1; then y = <*(F . the Element of dx)*> . z by A20, FINSEQ_1:40; hence z in <*(F . the Element of dx)*> " {y} by A18, A27, A26, FUNCT_1:def_7; ::_thesis: verum end; <*(F . the Element of dx)*> " {y} c= {1} by A18, RELAT_1:132; then <*(F . the Element of dx)*> " {y} = {1} by A25, XBOOLE_0:def_10; hence card ((F | { the Element of dx}) " {y}) = card FF by A24, CARD_1:30; ::_thesis: verum end; caseA28: y <> F . the Element of dx ; ::_thesis: card ((F | { the Element of dx}) " {y}) = card FF A29: now__::_thesis:_not_<*(F_._the_Element_of_dx)*>_"_{y}_<>_{} set z = the Element of <*(F . the Element of dx)*> " {y}; assume A30: <*(F . the Element of dx)*> " {y} <> {} ; ::_thesis: contradiction then <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} in {y} by FUNCT_1:def_7; then A31: <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} = y by TARSKI:def_1; the Element of <*(F . the Element of dx)*> " {y} in {1} by A18, A30, FUNCT_1:def_7; then the Element of <*(F . the Element of dx)*> " {y} = 1 by TARSKI:def_1; hence contradiction by A28, A31, FINSEQ_1:40; ::_thesis: verum end; now__::_thesis:_not_(F_|_{_the_Element_of_dx})_"_{y}_<>_{} set z = the Element of (F | { the Element of dx}) " {y}; assume A32: (F | { the Element of dx}) " {y} <> {} ; ::_thesis: contradiction then (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} in {y} by FUNCT_1:def_7; then A33: (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} = y by TARSKI:def_1; A34: the Element of (F | { the Element of dx}) " {y} in { the Element of dx} by A17, A32, FUNCT_1:def_7; then the Element of (F | { the Element of dx}) " {y} = the Element of dx by TARSKI:def_1; hence contradiction by A17, A28, A34, A33, FUNCT_1:47; ::_thesis: verum end; hence card ((F | { the Element of dx}) " {y}) = card FF by A29; ::_thesis: verum end; end; end; ((F | (X \ { the Element of dx})) " {y}) /\ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) /\ ((F | { the Element of dx}) " {y}) by FUNCT_1:70 .= ((X \ { the Element of dx}) /\ (F " {y})) /\ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70 .= (((F " {y}) /\ (X \ { the Element of dx})) /\ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:16 .= ((F " {y}) /\ ((X \ { the Element of dx}) /\ { the Element of dx})) /\ (F " {y}) by XBOOLE_1:16 .= {} /\ (F " {y}) by A14, XBOOLE_0:def_7 .= {} ; hence card (Coim ((F | X),y)) = ((card ((F | (X \ { the Element of dx})) " {y})) + (card FF)) - (card {}) by A15, A19, CARD_2:45 .= card (Coim (A,y)) by A16, FINSEQ_3:57 ; ::_thesis: verum end; hence F | X,A are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; theorem :: RFINSEQ:5 for F being Function for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent proof let F be Function; ::_thesis: for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent let X be finite set ; ::_thesis: ex f being FinSequence st F | X,f are_fiberwise_equipotent A1: card (dom (F | X)) = card (dom (F | X)) ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(Lm1, Lm2); hence ex f being FinSequence st F | X,f are_fiberwise_equipotent by A1; ::_thesis: verum end; definition let n be Nat; let f be FinSequence; funcf /^ n -> FinSequence means :Def1: :: RFINSEQ:def 1 ( len it = (len f) - n & ( for m being Nat st m in dom it holds it . m = f . (m + n) ) ) if n <= len f otherwise it = {} ; existence ( ( n <= len f implies ex b1 being FinSequence st ( len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds b1 . m = f . (m + n) ) ) ) & ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) ) proof thus ( n <= len f implies ex p1 being FinSequence st ( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds p1 . m = f . (m + n) ) ) ) ::_thesis: ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) proof assume n <= len f ; ::_thesis: ex p1 being FinSequence st ( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds p1 . m = f . (m + n) ) ) then reconsider k = (len f) - n as Element of NAT by NAT_1:21; deffunc H1( Nat) -> set = f . ($1 + n); consider p being FinSequence such that A1: ( len p = k & ( for m being Nat st m in dom p holds p . m = H1(m) ) ) from FINSEQ_1:sch_2(); take p ; ::_thesis: ( len p = (len f) - n & ( for m being Nat st m in dom p holds p . m = f . (m + n) ) ) thus len p = (len f) - n by A1; ::_thesis: for m being Nat st m in dom p holds p . m = f . (m + n) let m be Nat; ::_thesis: ( m in dom p implies p . m = f . (m + n) ) assume m in dom p ; ::_thesis: p . m = f . (m + n) hence p . m = f . (m + n) by A1; ::_thesis: verum end; thus ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) ; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence holds ( ( n <= len f & len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds b1 . m = f . (m + n) ) & len b2 = (len f) - n & ( for m being Nat st m in dom b2 holds b2 . m = f . (m + n) ) implies b1 = b2 ) & ( not n <= len f & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let p1, p2 be FinSequence; ::_thesis: ( ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds p2 . m = f . (m + n) ) implies p1 = p2 ) & ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) ) thus ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds p2 . m = f . (m + n) ) implies p1 = p2 ) ::_thesis: ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) proof assume that n <= len f and A2: len p1 = (len f) - n and A3: for m being Nat st m in dom p1 holds p1 . m = f . (m + n) and A4: len p2 = (len f) - n and A5: for m being Nat st m in dom p2 holds p2 . m = f . (m + n) ; ::_thesis: p1 = p2 A6: ( dom p1 = Seg (len p1) & Seg (len p2) = dom p2 ) by FINSEQ_1:def_3; 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 A7: m in dom p1 ; ::_thesis: p1 . m = p2 . m then p1 . m = f . (m + n) by A3; hence p1 . m = p2 . m by A2, A4, A5, A6, A7; ::_thesis: verum end; hence p1 = p2 by A2, A4, FINSEQ_2:9; ::_thesis: verum end; thus ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) ; ::_thesis: verum end; consistency for b1 being FinSequence holds verum ; end; :: deftheorem Def1 defines /^ RFINSEQ:def_1_:_ for n being Nat for f, b3 being FinSequence holds ( ( n <= len f implies ( b3 = f /^ n iff ( len b3 = (len f) - n & ( for m being Nat st m in dom b3 holds b3 . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b3 = f /^ n iff b3 = {} ) ) ); definition let D be set ; let n be Nat; let f be FinSequence of D; :: original: /^ redefine funcf /^ n -> FinSequence of D; coherence f /^ n is FinSequence of D proof set p = f /^ n; percases ( n <= len f or len f < n ) ; supposeA1: n <= len f ; ::_thesis: f /^ n is FinSequence of D then reconsider k = (len f) - n as Element of NAT by NAT_1:21; A2: len (f /^ n) = k by A1, Def1; 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 Nat such that A3: m in dom (f /^ n) and A4: (f /^ n) . m = x by FINSEQ_2:10; m <= len (f /^ n) by A3, FINSEQ_3:25; then A5: m + n <= len f by A2, XREAL_1:19; A6: m <= m + n by NAT_1:11; 1 <= m by A3, FINSEQ_3:25; then 1 <= m + n by A6, XXREAL_0:2; then A7: m + n in dom f by A5, FINSEQ_3:25; (f /^ n) . m = f . (m + n) by A1, A3, Def1; hence x in rng f by A4, A7, FUNCT_1:def_3; ::_thesis: verum end; then rng (f /^ n) c= D by XBOOLE_1:1; hence f /^ n is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum end; suppose len f < n ; ::_thesis: f /^ n is FinSequence of D then f /^ n = <*> D by Def1; hence f /^ n is FinSequence of D ; ::_thesis: verum end; end; end; end; Lm3: for n being Nat for D being non empty set for f being FinSequence of D st len f <= n holds f | n = f proof let n be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st len f <= n holds f | n = f let D be non empty set ; ::_thesis: for f being FinSequence of D st len f <= n holds f | n = f let f be FinSequence of D; ::_thesis: ( len f <= n implies f | n = f ) A1: dom f = Seg (len f) by FINSEQ_1:def_3; assume len f <= n ; ::_thesis: f | n = f then ( f | n = f | (Seg n) & dom f c= Seg n ) by A1, FINSEQ_1:5, FINSEQ_1:def_15; hence f | n = f by RELAT_1:68; ::_thesis: verum end; theorem Th6: :: RFINSEQ:6 for D being non empty set for f being FinSequence of D for n, m being Nat st n in dom f & m in Seg n holds ( (f | n) . m = f . m & m in dom f ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for n, m being Nat st n in dom f & m in Seg n holds ( (f | n) . m = f . m & m in dom f ) let f be FinSequence of D; ::_thesis: for n, m being Nat st n in dom f & m in Seg n holds ( (f | n) . m = f . m & m in dom f ) let n, m be Nat; ::_thesis: ( n in dom f & m in Seg n implies ( (f | n) . m = f . m & m in dom f ) ) assume that A1: n in dom f and A2: m in Seg n ; ::_thesis: ( (f | n) . m = f . m & m in dom f ) A3: f | n = f | (Seg n) by FINSEQ_1:def_15; ( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def_3, FINSEQ_3:25; then A4: Seg n c= dom f by FINSEQ_1:5; then Seg n = (dom f) /\ (Seg n) by XBOOLE_1:28 .= dom (f | n) by A3, RELAT_1:61 ; hence ( (f | n) . m = f . m & m in dom f ) by A2, A3, A4, FUNCT_1:47; ::_thesis: verum end; theorem Th7: :: RFINSEQ:7 for D being non empty set for f being FinSequence of D for n being Nat for x being set st len f = n + 1 & x = f . (n + 1) holds f = (f | n) ^ <*x*> proof let D be non empty set ; ::_thesis: for f being FinSequence of D for n being Nat for x being set st len f = n + 1 & x = f . (n + 1) holds f = (f | n) ^ <*x*> let f be FinSequence of D; ::_thesis: for n being Nat for x being set st len f = n + 1 & x = f . (n + 1) holds f = (f | n) ^ <*x*> let n be Nat; ::_thesis: for x being set st len f = n + 1 & x = f . (n + 1) holds f = (f | n) ^ <*x*> let x be set ; ::_thesis: ( len f = n + 1 & x = f . (n + 1) implies f = (f | n) ^ <*x*> ) assume that A1: len f = n + 1 and A2: x = f . (n + 1) ; ::_thesis: f = (f | n) ^ <*x*> set fn = f | n; A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11; A4: dom f = Seg (len f) by FINSEQ_1:def_3; A5: n <= n + 1 by NAT_1:11; A6: now__::_thesis:_for_m_being_Nat_st_m_in_dom_f_holds_ f_._m_=_((f_|_n)_^_<*x*>)_._m let m be Nat; ::_thesis: ( m in dom f implies f . m = ((f | n) ^ <*x*>) . m ) assume A7: m in dom f ; ::_thesis: f . m = ((f | n) ^ <*x*>) . m then A8: 1 <= m by A4, FINSEQ_1:1; A9: m <= len f by A4, A7, FINSEQ_1:1; now__::_thesis:_(_(_m_=_len_f_&_f_._m_=_((f_|_n)_^_<*x*>)_._m_)_or_(_m_<>_len_f_&_((f_|_n)_^_<*x*>)_._m_=_f_._m_)_) percases ( m = len f or m <> len f ) ; case m = len f ; ::_thesis: f . m = ((f | n) ^ <*x*>) . m hence f . m = ((f | n) ^ <*x*>) . m by A1, A2, A3, FINSEQ_1:42; ::_thesis: verum end; case m <> len f ; ::_thesis: ((f | n) ^ <*x*>) . m = f . m then m < n + 1 by A1, A9, XXREAL_0:1; then A10: m <= n by NAT_1:13; then 1 <= n by A8, XXREAL_0:2; then A11: n in dom f by A1, A5, FINSEQ_3:25; A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def_3; A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25; hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def_7 .= f . m by A3, A13, A11, A12, Th6 ; ::_thesis: verum end; end; end; hence f . m = ((f | n) ^ <*x*>) . m ; ::_thesis: verum end; len ((f | n) ^ <*x*>) = n + (len <*x*>) by A3, FINSEQ_1:22 .= len f by A1, FINSEQ_1:40 ; hence f = (f | n) ^ <*x*> by A6, FINSEQ_2:9; ::_thesis: verum end; theorem Th8: :: RFINSEQ:8 for D being non empty set for f being FinSequence of D for n being Nat holds (f | n) ^ (f /^ n) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for n being Nat holds (f | n) ^ (f /^ n) = f let f be FinSequence of D; ::_thesis: for n being Nat holds (f | n) ^ (f /^ n) = f let n be Nat; ::_thesis: (f | n) ^ (f /^ n) = f set fn = f /^ n; now__::_thesis:_(_(_len_f_<_n_&_(f_|_n)_^_(f_/^_n)_=_f_)_or_(_n_<=_len_f_&_(f_|_n)_^_(f_/^_n)_=_f_)_) percases ( len f < n or n <= len f ) ; case len f < n ; ::_thesis: (f | n) ^ (f /^ n) = f then ( f /^ n = <*> D & f | n = f ) by Def1, Lm3; hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; ::_thesis: verum end; caseA1: n <= len f ; ::_thesis: (f | n) ^ (f /^ n) = f A2: dom f = Seg (len f) by FINSEQ_1:def_3; A3: len (f | n) = n by A1, FINSEQ_1:59; A4: len (f /^ n) = (len f) - n by A1, Def1; then A5: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A3, FINSEQ_1:22 .= len f ; A6: dom (f | n) = Seg n by A3, FINSEQ_1:def_3; now__::_thesis:_for_m_being_Nat_st_m_in_dom_f_holds_ ((f_|_n)_^_(f_/^_n))_._m_=_f_._m let m be Nat; ::_thesis: ( m in dom f implies ((f | n) ^ (f /^ n)) . m = f . m ) assume A7: m in dom f ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . m then A8: m <= len f by A2, FINSEQ_1:1; A9: 1 <= m by A2, A7, FINSEQ_1:1; now__::_thesis:_(_(_m_<=_n_&_((f_|_n)_^_(f_/^_n))_._m_=_f_._m_)_or_(_n_<_m_&_((f_|_n)_^_(f_/^_n))_._m_=_f_._m_)_) percases ( m <= n or n < m ) ; caseA10: m <= n ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . m then 1 <= n by A9, XXREAL_0:2; then A11: n in dom f by A1, FINSEQ_3:25; A12: m in Seg n by A9, A10, FINSEQ_1:1; hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A6, FINSEQ_1:def_7 .= f . m by A12, A11, Th6 ; ::_thesis: verum end; caseA13: n < m ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . 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; n + 1 <= m by A13, NAT_1:13; then A14: 1 <= k by XREAL_1:19; k <= len (f /^ n) by A4, A8, XREAL_1:9; then A15: k in dom (f /^ n) by A14, FINSEQ_3:25; thus ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A3, A5, A8, A13, FINSEQ_1:24 .= f . (k + n) by A1, A15, Def1 .= f . m ; ::_thesis: verum end; end; end; hence ((f | n) ^ (f /^ n)) . m = f . m ; ::_thesis: verum end; hence (f | n) ^ (f /^ n) = f by A5, FINSEQ_2:9; ::_thesis: verum end; end; end; hence (f | n) ^ (f /^ n) = f ; ::_thesis: verum end; theorem :: RFINSEQ:9 for R1, R2 being FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds Sum R1 = Sum R2 proof let R1, R2 be FinSequence of REAL ; ::_thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 ) defpred S2[ Nat] means for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent & len f = $1 holds Sum f = Sum g; assume A1: R1,R2 are_fiberwise_equipotent ; ::_thesis: Sum R1 = Sum R2 A2: len R1 = len R1 ; A3: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A4: S2[n] ; ::_thesis: S2[n + 1] let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies Sum f = Sum g ) assume that A5: f,g are_fiberwise_equipotent and A6: len f = n + 1 ; ::_thesis: Sum f = Sum g set a = f . (n + 1); A7: rng f = rng g by A5, CLASSES1:75; 0 < n + 1 by NAT_1:3; then 0 + 1 <= n + 1 by NAT_1:13; then n + 1 in dom f by A6, FINSEQ_3:25; then f . (n + 1) in rng g by A7, FUNCT_1:def_3; then consider m being Nat such that A8: m in dom g and A9: g . m = f . (n + 1) by FINSEQ_2:10; set gg = g /^ m; set gm = g | m; m <= len g by A8, FINSEQ_3:25; then A10: len (g | m) = m by FINSEQ_1:59; A11: 1 <= m by A8, FINSEQ_3:25; then max (0,(m - 1)) = m - 1 by FINSEQ_2:4; then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5; A12: m = m1 + 1 ; then m1 <= m by NAT_1:11; then A13: Seg m1 c= Seg m by FINSEQ_1:5; m in Seg m by A11, FINSEQ_1:1; then (g | m) . m = f . (n + 1) by A8, A9, Th6; then A14: g | m = ((g | m) | m1) ^ <*(f . (n + 1))*> by A10, A12, Th7; set fn = f | n; A15: g = (g | m) ^ (g /^ m) by Th8; A16: (g | m) | m1 = (g | m) | (Seg m1) by FINSEQ_1:def_15 .= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def_15 .= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71 .= g | (Seg m1) by A13, XBOOLE_1:28 .= g | m1 by FINSEQ_1:def_15 ; A17: f = (f | n) ^ <*(f . (n + 1))*> by A6, Th7; now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_(((g_|_m1)_^_(g_/^_m)),x)) let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) card (Coim (f,x)) = card (Coim (g,x)) by A5, CLASSES1:def_9; then (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card ((((g | m1) ^ <*(f . (n + 1))*>) ^ (g /^ m)) " {x}) by A15, A14, A16, A17, FINSEQ_3:57 .= (card (((g | m1) ^ <*(f . (n + 1))*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57 .= ((card ((g | m1) " {x})) + (card (<*(f . (n + 1))*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57 .= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*(f . (n + 1))*> " {x})) .= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*(f . (n + 1))*> " {x})) by FINSEQ_3:57 ; hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; ::_thesis: verum end; then A18: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def_9; len (f | n) = n by A6, FINSEQ_1:59, NAT_1:11; then Sum (f | n) = Sum ((g | m1) ^ (g /^ m)) by A4, A18; hence Sum f = (Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f . (n + 1))*>) by A17, RVSUM_1:75 .= ((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f . (n + 1))*>) by RVSUM_1:75 .= ((Sum (g | m1)) + (Sum <*(f . (n + 1))*>)) + (Sum (g /^ m)) .= (Sum (g | m)) + (Sum (g /^ m)) by A14, A16, RVSUM_1:75 .= Sum g by A15, RVSUM_1:75 ; ::_thesis: verum end; A19: S2[ 0 ] proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Sum f = Sum g ) assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; ::_thesis: Sum f = Sum g then A20: ( len g = 0 & f = <*> REAL ) by Th3; then g = <*> REAL ; hence Sum f = Sum g by A20; ::_thesis: verum end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A19, A3); hence Sum R1 = Sum R2 by A1, A2; ::_thesis: verum end; definition let R be FinSequence of REAL ; func MIM R -> FinSequence of REAL means :Def2: :: RFINSEQ:def 2 ( len it = len R & it . (len it) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len it) - 1 holds it . n = (R . n) - (R . (n + 1)) ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) ) proof percases ( len R = 0 or len R <> 0 ) ; supposeA1: len R = 0 ; ::_thesis: ex b1 being FinSequence of REAL st ( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) ) take a = R; ::_thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds a . n = (R . n) - (R . (n + 1)) ) ) thus ( len a = len R & a . (len a) = R . (len R) ) ; ::_thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds a . n = (R . n) - (R . (n + 1)) let n be Nat; ::_thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) ) assume ( 1 <= n & n <= (len a) - 1 ) ; ::_thesis: a . n = (R . n) - (R . (n + 1)) hence a . n = (R . n) - (R . (n + 1)) by A1, XXREAL_0:2; ::_thesis: verum end; suppose len R <> 0 ; ::_thesis: ex b1 being FinSequence of REAL st ( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) ) then 0 < len R by NAT_1:3; then 0 + 1 <= len R by NAT_1:13; then max (0,((len R) - 1)) = (len R) - 1 by FINSEQ_2:4; then reconsider l = (len R) - 1 as Element of NAT by FINSEQ_2:5; defpred S2[ Nat, set ] means $2 = (R . $1) - (R . ($1 + 1)); set t = R . (len R); A2: for n being Nat st n in Seg l holds ex x being Real st S2[n,x] ; consider p being FinSequence of REAL such that A3: ( dom p = Seg l & ( for n being Nat st n in Seg l holds S2[n,p . n] ) ) from FINSEQ_1:sch_5(A2); take a = p ^ <*(R . (len R))*>; ::_thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds a . n = (R . n) - (R . (n + 1)) ) ) thus A4: len a = (len p) + (len <*(R . (len R))*>) by FINSEQ_1:22 .= l + (len <*(R . (len R))*>) by A3, FINSEQ_1:def_3 .= l + 1 by FINSEQ_1:39 .= len R ; ::_thesis: ( a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds a . n = (R . n) - (R . (n + 1)) ) ) hence a . (len a) = a . (l + 1) .= a . ((len p) + 1) by A3, FINSEQ_1:def_3 .= R . (len R) by FINSEQ_1:42 ; ::_thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds a . n = (R . n) - (R . (n + 1)) let n be Nat; ::_thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) ) assume ( 1 <= n & n <= (len a) - 1 ) ; ::_thesis: a . n = (R . n) - (R . (n + 1)) then A5: n in Seg l by A4, FINSEQ_1:1; then p . n = (R . n) - (R . (n + 1)) by A3; hence a . n = (R . n) - (R . (n + 1)) by A3, A5, FINSEQ_1:def_7; ::_thesis: verum end; end; end; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds b1 . n = (R . n) - (R . (n + 1)) ) & len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds b2 . n = (R . n) - (R . (n + 1)) ) holds b1 = b2 proof let p1, p2 be FinSequence of REAL ; ::_thesis: ( len p1 = len R & p1 . (len p1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p1) - 1 holds p1 . n = (R . n) - (R . (n + 1)) ) & len p2 = len R & p2 . (len p2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p2) - 1 holds p2 . n = (R . n) - (R . (n + 1)) ) implies p1 = p2 ) assume that A6: len p1 = len R and A7: p1 . (len p1) = R . (len R) and A8: for n being Nat st 1 <= n & n <= (len p1) - 1 holds p1 . n = (R . n) - (R . (n + 1)) and A9: len p2 = len R and A10: p2 . (len p2) = R . (len R) and A11: for n being Nat st 1 <= n & n <= (len p2) - 1 holds p2 . n = (R . n) - (R . (n + 1)) ; ::_thesis: p1 = p2 A12: dom p1 = Seg (len R) by A6, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_p1_holds_ p1_._n_=_p2_._n let n be Nat; ::_thesis: ( n in dom p1 implies p1 . n = p2 . n ) set r = R . n; assume A13: n in dom p1 ; ::_thesis: p1 . n = p2 . n then A14: 1 <= n by A12, FINSEQ_1:1; A15: n <= len R by A12, A13, FINSEQ_1:1; now__::_thesis:_(_(_n_=_len_R_&_p1_._n_=_p2_._n_)_or_(_n_<>_len_R_&_p1_._n_=_p2_._n_)_) percases ( n = len R or n <> len R ) ; case n = len R ; ::_thesis: p1 . n = p2 . n hence p1 . n = p2 . n by A6, A7, A9, A10; ::_thesis: verum end; caseA16: n <> len R ; ::_thesis: p1 . n = p2 . n set s = R . (n + 1); n < len R by A15, A16, XXREAL_0:1; then n + 1 <= len R by NAT_1:13; then A17: n <= (len R) - 1 by XREAL_1:19; then p1 . n = (R . n) - (R . (n + 1)) by A6, A8, A14; hence p1 . n = p2 . n by A9, A11, A14, A17; ::_thesis: verum end; end; end; hence p1 . n = p2 . n ; ::_thesis: verum end; hence p1 = p2 by A6, A9, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def2 defines MIM RFINSEQ:def_2_:_ for R, b2 being FinSequence of REAL holds ( b2 = MIM R iff ( len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds b2 . n = (R . n) - (R . (n + 1)) ) ) ); theorem Th10: :: RFINSEQ:10 for R being FinSequence of REAL for r being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r holds MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*> proof let R be FinSequence of REAL ; ::_thesis: for r being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r holds MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*> let s be Real; ::_thesis: for n being Element of NAT st len R = n + 2 & R . (n + 1) = s holds MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> let n be Element of NAT ; ::_thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> ) assume that A1: len R = n + 2 and A2: R . (n + 1) = s ; ::_thesis: MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> set f1 = R | (n + 1); set m1 = MIM (R | (n + 1)); set mf = MIM R; set fn = (MIM R) | n; 0 < n + 1 by NAT_1:3; then A3: 0 + 1 <= n + 1 by NAT_1:13; A4: (n + 1) + 1 = n + (1 + 1) ; then n + 1 <= n + 2 by NAT_1:11; then A5: ( Seg (len R) = dom R & n + 1 in Seg (n + 2) ) by A3, FINSEQ_1:1, FINSEQ_1:def_3; A6: len (R | (n + 1)) = n + 1 by A1, A4, FINSEQ_1:59, NAT_1:11; then A7: len (MIM (R | (n + 1))) = n + 1 by Def2; then A8: dom (MIM (R | (n + 1))) = Seg (n + 1) by FINSEQ_1:def_3; n + 1 in Seg (n + 1) by A3, FINSEQ_1:1; then (R | (n + 1)) . (n + 1) = s by A1, A2, A5, Th6; then A9: (MIM (R | (n + 1))) . (n + 1) = s by A6, A7, Def2; A10: Seg (len ((MIM R) | n)) = dom ((MIM R) | n) by FINSEQ_1:def_3; A11: Seg (len (MIM R)) = dom (MIM R) by FINSEQ_1:def_3; A12: len (MIM R) = n + 2 by A1, Def2; then A13: len ((MIM R) | n) = n by FINSEQ_1:59, NAT_1:11; A14: n <= n + 2 by NAT_1:11; A15: now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_(R_|_(n_+_1)))_holds_ (MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m let m be Nat; ::_thesis: ( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ) assume A16: m in dom (MIM (R | (n + 1))) ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m then A17: 1 <= m by A8, FINSEQ_1:1; A18: m <= n + 1 by A8, A16, FINSEQ_1:1; now__::_thesis:_(_(_m_=_n_+_1_&_(MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m_)_or_(_m_<>_n_+_1_&_(MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m_)_) percases ( m = n + 1 or m <> n + 1 ) ; case m = n + 1 ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A13, A9, FINSEQ_1:42; ::_thesis: verum end; case m <> n + 1 ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m then A19: m < n + 1 by A18, XXREAL_0:1; then A20: m <= n by NAT_1:13; then A21: m in Seg n by A17, FINSEQ_1:1; set r2 = R . (m + 1); set r1 = R . m; A22: (len (MIM R)) - 1 = n + 1 by A12; 1 <= n by A17, A20, XXREAL_0:2; then n in Seg (n + 2) by A14, FINSEQ_1:1; then ((MIM R) | n) . m = (MIM R) . m by A12, A11, A21, Th6; then A23: (R . m) - (R . (m + 1)) = ((MIM R) | n) . m by A17, A18, A22, Def2 .= (((MIM R) | n) ^ <*s*>) . m by A13, A10, A21, FINSEQ_1:def_7 ; ( 1 <= m + 1 & m + 1 <= n + 1 ) by A19, NAT_1:11, NAT_1:13; then m + 1 in Seg (n + 1) by FINSEQ_1:1; then A24: (R | (n + 1)) . (m + 1) = R . (m + 1) by A1, A5, Th6; ( (len (MIM (R | (n + 1)))) - 1 = n & (R | (n + 1)) . m = R . m ) by A1, A7, A5, A8, A16, Th6; hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A17, A20, A23, A24, Def2; ::_thesis: verum end; end; end; hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ; ::_thesis: verum end; len (((MIM R) | n) ^ <*s*>) = n + (len <*s*>) by A13, FINSEQ_1:22 .= n + 1 by FINSEQ_1:40 ; hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by A7, A15, FINSEQ_2:9; ::_thesis: verum end; theorem Th11: :: RFINSEQ:11 for R being FinSequence of REAL for r, s being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds MIM R = ((MIM R) | n) ^ <*(r - s),s*> proof let R be FinSequence of REAL ; ::_thesis: for r, s being Real for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds MIM R = ((MIM R) | n) ^ <*(r - s),s*> let r, s be Real; ::_thesis: for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds MIM R = ((MIM R) | n) ^ <*(r - s),s*> let n be Element of NAT ; ::_thesis: ( len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s implies MIM R = ((MIM R) | n) ^ <*(r - s),s*> ) set mf = MIM R; set nf = (MIM R) | n; assume that A1: len R = n + 2 and A2: R . (n + 1) = r and A3: R . (n + 2) = s ; ::_thesis: MIM R = ((MIM R) | n) ^ <*(r - s),s*> A4: len (MIM R) = n + 2 by A1, Def2; then A5: dom (MIM R) = Seg (n + 2) by FINSEQ_1:def_3; A6: n + (1 + 1) = (n + 1) + 1 ; then n + 1 <= n + 2 by NAT_1:11; then A7: n < n + 2 by NAT_1:13; A8: len ((MIM R) | n) = n by A4, FINSEQ_1:59, NAT_1:11; then len (((MIM R) | n) ^ <*(r - s),s*>) = n + (len <*(r - s),s*>) by FINSEQ_1:22; then A9: len (((MIM R) | n) ^ <*(r - s),s*>) = n + 2 by FINSEQ_1:44; A10: n <= n + 2 by NAT_1:11; now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_R)_holds_ (MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m let m be Nat; ::_thesis: ( m in dom (MIM R) implies (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ) assume A11: m in dom (MIM R) ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m then A12: 1 <= m by A5, FINSEQ_1:1; A13: m <= n + 2 by A5, A11, FINSEQ_1:1; now__::_thesis:_(_(_m_=_n_+_2_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_or_(_m_<>_n_+_2_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_) percases ( m = n + 2 or m <> n + 2 ) ; caseA14: m = n + 2 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m hence (MIM R) . m = s by A1, A3, A4, Def2 .= <*(r - s),s*> . ((n + 2) - n) by FINSEQ_1:44 .= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A7, A14, FINSEQ_1:24 ; ::_thesis: verum end; case m <> n + 2 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m then m < n + 2 by A13, XXREAL_0:1; then A15: m <= n + 1 by A6, NAT_1:13; A16: (len (MIM R)) - 1 = n + 1 by A4; now__::_thesis:_(_(_m_=_n_+_1_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_or_(_m_<>_n_+_1_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_) percases ( m = n + 1 or m <> n + 1 ) ; caseA17: m = n + 1 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m then A18: n < m by NAT_1:13; thus (MIM R) . m = r - s by A2, A3, A6, A12, A16, A17, Def2 .= <*(r - s),s*> . ((n + 1) - n) by FINSEQ_1:44 .= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A13, A17, A18, FINSEQ_1:24 ; ::_thesis: verum end; case m <> n + 1 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m then m < n + 1 by A15, XXREAL_0:1; then A19: m <= n by NAT_1:13; then A20: m in Seg n by A12, FINSEQ_1:1; 1 <= n by A12, A19, XXREAL_0:2; then A21: n in Seg (n + 2) by A10, FINSEQ_1:1; A22: dom ((MIM R) | n) = Seg (len ((MIM R) | n)) by FINSEQ_1:def_3; dom (MIM R) = Seg (len (MIM R)) by FINSEQ_1:def_3; hence (MIM R) . m = ((MIM R) | n) . m by A4, A20, A21, Th6 .= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A20, A22, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; ::_thesis: verum end; end; end; hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; ::_thesis: verum end; hence MIM R = ((MIM R) | n) ^ <*(r - s),s*> by A4, A9, FINSEQ_2:9; ::_thesis: verum end; theorem Th12: :: RFINSEQ:12 MIM (<*> REAL) = <*> REAL proof set o = <*> REAL; set mo = MIM (<*> REAL); len (MIM (<*> REAL)) = len (<*> REAL) by Def2; hence MIM (<*> REAL) = <*> REAL ; ::_thesis: verum end; theorem Th13: :: RFINSEQ:13 for r being Real holds MIM <*r*> = <*r*> proof let r be Real; ::_thesis: MIM <*r*> = <*r*> set f = <*r*>; A1: len <*r*> = 1 by FINSEQ_1:40; then A2: len (MIM <*r*>) = 1 by Def2; then A3: dom (MIM <*r*>) = Seg 1 by FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_(MIM_<*r*>)_holds_ (MIM_<*r*>)_._n_=_<*r*>_._n let n be Nat; ::_thesis: ( n in dom (MIM <*r*>) implies (MIM <*r*>) . n = <*r*> . n ) assume n in dom (MIM <*r*>) ; ::_thesis: (MIM <*r*>) . n = <*r*> . n then n = 1 by A3, FINSEQ_1:2, TARSKI:def_1; hence (MIM <*r*>) . n = <*r*> . n by A1, A2, Def2; ::_thesis: verum end; hence MIM <*r*> = <*r*> by A1, A2, FINSEQ_2:9; ::_thesis: verum end; theorem :: RFINSEQ:14 for r, s being Real holds MIM <*r,s*> = <*(r - s),s*> proof let r, s be Real; ::_thesis: MIM <*r,s*> = <*(r - s),s*> set f = <*r,s*>; A1: ( len <*r,s*> = 2 & <*r,s*> . 1 = r ) by FINSEQ_1:44; A2: <*r,s*> . 2 = s by FINSEQ_1:44; ( 0 + 2 = 2 & 0 + 1 = 1 ) ; then MIM <*r,s*> = ((MIM <*r,s*>) | 0) ^ <*(r - s),s*> by A1, A2, Th11; hence MIM <*r,s*> = <*(r - s),s*> by FINSEQ_1:34; ::_thesis: verum end; theorem :: RFINSEQ:15 for R being FinSequence of REAL for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n) proof let R be FinSequence of REAL ; ::_thesis: for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n) let n be Element of NAT ; ::_thesis: (MIM R) /^ n = MIM (R /^ n) set mf = MIM R; set fn = R /^ n; set mn = MIM (R /^ n); A1: len (MIM R) = len R by Def2; A2: len (MIM (R /^ n)) = len (R /^ n) by Def2; now__::_thesis:_(_(_len_R_<_n_&_(MIM_R)_/^_n_=_MIM_(R_/^_n)_)_or_(_n_<=_len_R_&_(MIM_R)_/^_n_=_MIM_(R_/^_n)_)_) percases ( len R < n or n <= len R ) ; caseA3: len R < n ; ::_thesis: (MIM R) /^ n = MIM (R /^ n) then (MIM R) /^ n = <*> REAL by A1, Def1; hence (MIM R) /^ n = MIM (R /^ n) by A3, Def1, Th12; ::_thesis: verum end; caseA4: n <= len R ; ::_thesis: (MIM R) /^ n = MIM (R /^ n) then A5: len ((MIM R) /^ n) = (len R) - n by A1, Def1; A6: len (MIM (R /^ n)) = len (R /^ n) by Def2; then A7: dom (MIM (R /^ n)) = Seg (len (R /^ n)) by FINSEQ_1:def_3; A8: Seg (len ((MIM R) /^ n)) = dom ((MIM R) /^ n) by FINSEQ_1:def_3; A9: len (R /^ n) = (len R) - n by A4, Def1; A10: Seg (len (R /^ n)) = dom (R /^ n) by FINSEQ_1:def_3; now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_(R_/^_n))_holds_ ((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m let m be Nat; ::_thesis: ( m in dom (MIM (R /^ n)) implies ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ) set r1 = R . (m + n); assume A11: m in dom (MIM (R /^ n)) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m then A12: 1 <= m by A7, FINSEQ_1:1; A13: m <= len (R /^ n) by A7, A11, FINSEQ_1:1; A14: (R /^ n) . m = R . (m + n) by A4, A10, A7, A11, Def1; m <= m + n by NAT_1:11; then A15: 1 <= m + n by A12, XXREAL_0:2; now__::_thesis:_(_(_m_=_len_(R_/^_n)_&_((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m_)_or_(_m_<>_len_(R_/^_n)_&_((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m_)_) percases ( m = len (R /^ n) or m <> len (R /^ n) ) ; caseA16: m = len (R /^ n) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1 .= R . (m + n) by A1, A9, A16, Def2 .= (MIM (R /^ n)) . m by A6, A14, A16, Def2 ; ::_thesis: verum end; case m <> len (R /^ n) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m then m < len (R /^ n) by A13, XXREAL_0:1; then A17: m + 1 <= len (R /^ n) by NAT_1:13; then A18: m <= (len (R /^ n)) - 1 by XREAL_1:19; set r2 = R . ((m + 1) + n); A19: (m + 1) + n = (m + n) + 1 ; 1 <= m + 1 by NAT_1:11; then m + 1 in dom (R /^ n) by A17, FINSEQ_3:25; then A20: (R /^ n) . (m + 1) = R . ((m + 1) + n) by A4, Def1; (m + 1) + n <= len R by A9, A17, XREAL_1:19; then A21: m + n <= (len R) - 1 by A19, XREAL_1:19; thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1 .= (R . (m + n)) - (R . ((m + 1) + n)) by A1, A15, A19, A21, Def2 .= (MIM (R /^ n)) . m by A2, A12, A14, A18, A20, Def2 ; ::_thesis: verum end; end; end; hence ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ; ::_thesis: verum end; hence (MIM R) /^ n = MIM (R /^ n) by A5, A9, A6, FINSEQ_2:9; ::_thesis: verum end; end; end; hence (MIM R) /^ n = MIM (R /^ n) ; ::_thesis: verum end; theorem Th16: :: RFINSEQ:16 for R being FinSequence of REAL st len R <> 0 holds Sum (MIM R) = R . 1 proof defpred S2[ Nat] means for R being FinSequence of REAL st len R <> 0 & len R = $1 holds Sum (MIM R) = R . 1; let R be FinSequence of REAL ; ::_thesis: ( len R <> 0 implies Sum (MIM R) = R . 1 ) assume A1: len R <> 0 ; ::_thesis: Sum (MIM R) = R . 1 A2: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A3: S2[n] ; ::_thesis: S2[n + 1] let R be FinSequence of REAL ; ::_thesis: ( len R <> 0 & len R = n + 1 implies Sum (MIM R) = R . 1 ) assume that len R <> 0 and A4: len R = n + 1 ; ::_thesis: Sum (MIM R) = R . 1 now__::_thesis:_(_(_n_=_0_&_Sum_(MIM_R)_=_R_._1_)_or_(_n_<>_0_&_Sum_(MIM_R)_=_R_._1_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: Sum (MIM R) = R . 1 then A5: R = <*(R . 1)*> by A4, FINSEQ_1:40; then MIM R = R by Th13; hence Sum (MIM R) = R . 1 by A5, FINSOP_1:11; ::_thesis: verum end; case n <> 0 ; ::_thesis: Sum (MIM R) = R . 1 then 0 < n by NAT_1:3; then 0 + 1 <= n by NAT_1:13; then max (0,(n - 1)) = n - 1 by FINSEQ_2:4; then reconsider n1 = n - 1 as Element of NAT by FINSEQ_2:5; A6: 0 + 1 <= n1 + 1 by NAT_1:11; then A7: ( Seg (len R) = dom R & 1 in Seg (n1 + 1) ) by FINSEQ_1:1, FINSEQ_1:def_3; n1 + 2 = (n1 + 1) + 1 ; then n1 + 1 <= n1 + 2 by NAT_1:11; then A8: n1 + 1 in Seg (n1 + 2) by A6, FINSEQ_1:1; set f1 = R | (n1 + 1); set s = R . (n1 + 2); set r = R . (n1 + 1); A9: n1 + 2 = len R by A4; A10: len (R | (n1 + 1)) = n1 + 1 by A4, FINSEQ_1:59, NAT_1:11; thus Sum (MIM R) = Sum (((MIM R) | n1) ^ <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by A4, Th11 .= (Sum ((MIM R) | n1)) + (Sum <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by RVSUM_1:75 .= (Sum ((MIM R) | n1)) + (((R . (n1 + 1)) - (R . (n1 + 2))) + (R . (n1 + 2))) by RVSUM_1:77 .= Sum (((MIM R) | n1) ^ <*(R . (n1 + 1))*>) by RVSUM_1:74 .= Sum (MIM (R | (n1 + 1))) by A9, Th10 .= (R | (n1 + 1)) . 1 by A3, A10 .= R . 1 by A4, A8, A7, Th6 ; ::_thesis: verum end; end; end; hence Sum (MIM R) = R . 1 ; ::_thesis: verum end; A11: S2[ 0 ] ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A11, A2); hence Sum (MIM R) = R . 1 by A1; ::_thesis: verum end; theorem :: RFINSEQ:17 for R being FinSequence of REAL for n being Element of NAT st n < len R holds Sum (MIM (R /^ n)) = R . (n + 1) proof let R be FinSequence of REAL ; ::_thesis: for n being Element of NAT st n < len R holds Sum (MIM (R /^ n)) = R . (n + 1) let n be Element of NAT ; ::_thesis: ( n < len R implies Sum (MIM (R /^ n)) = R . (n + 1) ) assume A1: n < len R ; ::_thesis: Sum (MIM (R /^ n)) = R . (n + 1) then A2: len (R /^ n) = (len R) - n by Def1; n + 1 <= len R by A1, NAT_1:13; then 1 <= (len R) - n by XREAL_1:19; then A3: 1 in dom (R /^ n) by A2, FINSEQ_3:25; len (R /^ n) <> 0 by A1, A2; hence Sum (MIM (R /^ n)) = (R /^ n) . 1 by Th16 .= R . (n + 1) by A1, A3, Def1 ; ::_thesis: verum end; definition let IT be FinSequence of REAL ; redefine attr IT is non-increasing means :Def3: :: RFINSEQ:def 3 for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1); compatibility ( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ) proof thus ( IT is non-increasing implies for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ) ::_thesis: ( ( for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ) implies IT is non-increasing ) proof assume A1: IT is non-increasing ; ::_thesis: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) let n be Element of NAT ; ::_thesis: ( n in dom IT & n + 1 in dom IT implies IT . n >= IT . (n + 1) ) assume A2: ( n in dom IT & n + 1 in dom IT ) ; ::_thesis: IT . n >= IT . (n + 1) n + 0 <= n + 1 by XREAL_1:6; hence IT . n >= IT . (n + 1) by A1, A2, SEQM_3:def_4; ::_thesis: verum end; assume A3: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ; ::_thesis: IT is non-increasing let m be Element of NAT ; :: according to SEQM_3:def_4 ::_thesis: for b1 being Element of NAT holds ( not m in dom IT or not b1 in dom IT or not m <= b1 or IT . b1 <= IT . m ) let n be Element of NAT ; ::_thesis: ( not m in dom IT or not n in dom IT or not m <= n or IT . n <= IT . m ) assume that A4: m in dom IT and A5: ( n in dom IT & m <= n ) ; ::_thesis: IT . n <= IT . m defpred S2[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 ); A6: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume that A7: S2[k] and A8: k + 1 in dom IT ; ::_thesis: ( not m <= k + 1 or IT . m >= IT . (k + 1) ) assume m <= k + 1 ; ::_thesis: IT . m >= IT . (k + 1) then A9: ( m < k + 1 or m = k + 1 ) by XXREAL_0:1; percases ( m <= k or m = k + 1 ) by A9, NAT_1:13; supposeA10: m <= k ; ::_thesis: IT . m >= IT . (k + 1) ( k + 0 <= k + 1 & k + 1 <= len IT ) by A8, FINSEQ_3:25, XREAL_1:6; then A11: k <= len IT by XXREAL_0:2; 1 <= m by A4, FINSEQ_3:25; then A12: 1 <= k by A10, XXREAL_0:2; then k in dom IT by A11, FINSEQ_3:25; then IT . k >= IT . (k + 1) by A3, A8; hence IT . m >= IT . (k + 1) by A7, A10, A12, A11, FINSEQ_3:25, XXREAL_0:2; ::_thesis: verum end; suppose m = k + 1 ; ::_thesis: IT . m >= IT . (k + 1) hence IT . m >= IT . (k + 1) ; ::_thesis: verum end; end; end; A13: S2[ 0 ] by FINSEQ_3:24; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A13, A6); hence IT . n <= IT . m by A5; ::_thesis: verum end; end; :: deftheorem Def3 defines non-increasing RFINSEQ:def_3_:_ for IT being FinSequence of REAL holds ( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n >= IT . (n + 1) ); registration cluster Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st b1 is non-increasing proof take <*> REAL ; ::_thesis: <*> REAL is non-increasing let n be Element of NAT ; :: according to RFINSEQ:def_3 ::_thesis: ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) ) thus ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) ) ; ::_thesis: verum end; end; theorem Th18: :: RFINSEQ:18 for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds R is non-increasing proof let R be FinSequence of REAL ; ::_thesis: ( ( len R = 0 or len R = 1 ) implies R is non-increasing ) assume A1: ( len R = 0 or len R = 1 ) ; ::_thesis: R is non-increasing now__::_thesis:_(_(_len_R_=_0_&_R_is_non-increasing_)_or_(_len_R_=_1_&_R_is_non-increasing_)_) percases ( len R = 0 or len R = 1 ) by A1; case len R = 0 ; ::_thesis: R is non-increasing then R = <*> REAL ; then for n being Element of NAT st n in dom R & n + 1 in dom R holds R . n >= R . (n + 1) ; hence R is non-increasing by Def3; ::_thesis: verum end; case len R = 1 ; ::_thesis: R is non-increasing then A2: dom R = {1} by FINSEQ_1:2, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_R_&_n_+_1_in_dom_R_holds_ R_._n_>=_R_._(n_+_1) let n be Element of NAT ; ::_thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) ) assume that A3: n in dom R and A4: n + 1 in dom R ; ::_thesis: R . n >= R . (n + 1) n = 1 by A2, A3, TARSKI:def_1; hence R . n >= R . (n + 1) by A2, A4, TARSKI:def_1; ::_thesis: verum end; hence R is non-increasing by Def3; ::_thesis: verum end; end; end; hence R is non-increasing ; ::_thesis: verum end; theorem Th19: :: RFINSEQ:19 for R being FinSequence of REAL holds ( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ) proof let R be FinSequence of REAL ; ::_thesis: ( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ) thus ( R is non-increasing implies for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ) ::_thesis: ( ( for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ) implies R is non-increasing ) proof defpred S2[ Nat] means ( $1 in dom R implies for n being Element of NAT st n in dom R & n < $1 holds R . n >= R . $1 ); assume A1: R is non-increasing ; ::_thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m A2: for m being Element of NAT st S2[m] holds S2[m + 1] proof let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A3: S2[m] ; ::_thesis: S2[m + 1] assume A4: m + 1 in dom R ; ::_thesis: for n being Element of NAT st n in dom R & n < m + 1 holds R . n >= R . (m + 1) then m + 1 <= len R by FINSEQ_3:25; then A5: m <= len R by NAT_1:13; let n be Element of NAT ; ::_thesis: ( n in dom R & n < m + 1 implies R . n >= R . (m + 1) ) assume that A6: n in dom R and A7: n < m + 1 ; ::_thesis: R . n >= R . (m + 1) set t = R . m; set r = R . n; set s = R . (m + 1); A8: n <= m by A7, NAT_1:13; 1 <= n by A6, FINSEQ_3:25; then A9: 1 <= m by A8, XXREAL_0:2; then A10: m in dom R by A5, FINSEQ_3:25; now__::_thesis:_(_(_n_=_m_&_R_._n_>=_R_._(m_+_1)_)_or_(_n_<>_m_&_R_._n_>=_R_._(m_+_1)_)_) percases ( n = m or n <> m ) ; case n = m ; ::_thesis: R . n >= R . (m + 1) hence R . n >= R . (m + 1) by A1, A4, A6, Def3; ::_thesis: verum end; case n <> m ; ::_thesis: R . n >= R . (m + 1) then n < m by A8, XXREAL_0:1; then A11: R . n >= R . m by A3, A6, A9, A5, FINSEQ_3:25; R . m >= R . (m + 1) by A1, A4, A10, Def3; hence R . n >= R . (m + 1) by A11, XXREAL_0:2; ::_thesis: verum end; end; end; hence R . n >= R . (m + 1) ; ::_thesis: verum end; Seg (len R) = dom R by FINSEQ_1:def_3; then A12: S2[ 0 ] by FINSEQ_1:1; for m being Element of NAT holds S2[m] from NAT_1:sch_1(A12, A2); hence for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ; ::_thesis: verum end; assume A13: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n >= R . m ; ::_thesis: R is non-increasing let n be Element of NAT ; :: according to RFINSEQ:def_3 ::_thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) ) A14: n < n + 1 by NAT_1:13; assume ( n in dom R & n + 1 in dom R ) ; ::_thesis: R . n >= R . (n + 1) hence R . n >= R . (n + 1) by A13, A14; ::_thesis: verum end; theorem Th20: :: RFINSEQ:20 for R being non-increasing FinSequence of REAL for n being Element of NAT holds R | n is non-increasing FinSequence of REAL proof let f be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f | n is non-increasing FinSequence of REAL let n be Element of NAT ; ::_thesis: f | n is non-increasing FinSequence of REAL set fn = f | n; now__::_thesis:_(_(_n_=_0_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_or_(_n_<>_0_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: f | n is non-increasing FinSequence of REAL then len (f | n) = 0 ; hence f | n is non-increasing FinSequence of REAL by Th18; ::_thesis: verum end; case n <> 0 ; ::_thesis: f | n is non-increasing FinSequence of REAL then 0 < n by NAT_1:3; then A1: 0 + 1 <= n by NAT_1:13; now__::_thesis:_(_(_len_f_<=_n_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_or_(_n_<_len_f_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_) percases ( len f <= n or n < len f ) ; case len f <= n ; ::_thesis: f | n is non-increasing FinSequence of REAL hence f | n is non-increasing FinSequence of REAL by Lm3; ::_thesis: verum end; case n < len f ; ::_thesis: f | n is non-increasing FinSequence of REAL then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:59, FINSEQ_3:25; now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_|_n)_&_m_+_1_in_dom_(f_|_n)_holds_ (f_|_n)_._m_>=_(f_|_n)_._(m_+_1) let m be Element of NAT ; ::_thesis: ( m in dom (f | n) & m + 1 in dom (f | n) implies (f | n) . m >= (f | n) . (m + 1) ) A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def_3; assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; ::_thesis: (f | n) . m >= (f | n) . (m + 1) then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, Th6; ( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, Th6; hence (f | n) . m >= (f | n) . (m + 1) by A5, Def3; ::_thesis: verum end; hence f | n is non-increasing FinSequence of REAL by Def3; ::_thesis: verum end; end; end; hence f | n is non-increasing FinSequence of REAL ; ::_thesis: verum end; end; end; hence f | n is non-increasing FinSequence of REAL ; ::_thesis: verum end; theorem :: RFINSEQ:21 for R being non-increasing FinSequence of REAL for n being Element of NAT holds R /^ n is non-increasing proof let f be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f /^ n is non-increasing let n be Element of NAT ; ::_thesis: f /^ n is non-increasing set fn = f /^ n; now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_/^_n)_&_m_+_1_in_dom_(f_/^_n)_holds_ (f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1) let m be Element of NAT ; ::_thesis: ( m in dom (f /^ n) & m + 1 in dom (f /^ n) implies (f /^ n) . m >= (f /^ n) . (m + 1) ) assume that A1: m in dom (f /^ n) and A2: m + 1 in dom (f /^ n) ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1) A3: m <= m + n by NAT_1:11; 1 <= m by A1, FINSEQ_3:25; then A4: 1 <= m + n by A3, XXREAL_0:2; A5: 1 <= (m + n) + 1 by NAT_1:11; A6: m + 1 <= len (f /^ n) by A2, FINSEQ_3:25; set r = (f /^ n) . m; set s = (f /^ n) . (m + 1); A7: (m + 1) + n = (m + n) + 1 ; A8: m <= len (f /^ n) by A1, FINSEQ_3:25; now__::_thesis:_(_(_n_<=_len_f_&_(f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1)_)_or_(_len_f_<_n_&_(f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1)_)_) percases ( n <= len f or len f < n ) ; caseA9: n <= len f ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1) then A10: len (f /^ n) = (len f) - n by Def1; then m + n <= len f by A8, XREAL_1:19; then A11: m + n in dom f by A4, FINSEQ_3:25; (m + n) + 1 <= len f by A6, A7, A10, XREAL_1:19; then A12: (m + n) + 1 in dom f by A5, FINSEQ_3:25; ( (f /^ n) . m = f . (m + n) & (f /^ n) . (m + 1) = f . ((m + n) + 1) ) by A1, A2, A7, A9, Def1; hence (f /^ n) . m >= (f /^ n) . (m + 1) by A11, A12, Def3; ::_thesis: verum end; case len f < n ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1) then f /^ n = <*> REAL by Def1; hence (f /^ n) . m >= (f /^ n) . (m + 1) ; ::_thesis: verum end; end; end; hence (f /^ n) . m >= (f /^ n) . (m + 1) ; ::_thesis: verum end; hence f /^ n is non-increasing by Def3; ::_thesis: verum end; Lm4: for f, g being non-increasing FinSequence of REAL for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) proof let f, g be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) let n be Element of NAT ; ::_thesis: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent implies ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) ) assume that A1: len f = n + 1 and A2: len f = len g and A3: f,g are_fiberwise_equipotent ; ::_thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) set r = f . (n + 1); set s = g . (n + 1); 0 < n + 1 by NAT_1:3; then A4: 0 + 1 <= n + 1 by NAT_1:13; then A5: n + 1 in dom f by A1, FINSEQ_3:25; A6: f = (f | n) ^ <*(f . (n + 1))*> by A1, Th7; A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25; A8: now__::_thesis:_not_f_._(n_+_1)_<>_g_._(n_+_1) A9: rng f = rng g by A3, CLASSES1:75; assume A10: f . (n + 1) <> g . (n + 1) ; ::_thesis: contradiction now__::_thesis:_(_(_f_._(n_+_1)_>_g_._(n_+_1)_&_contradiction_)_or_(_f_._(n_+_1)_<_g_._(n_+_1)_&_contradiction_)_) percases ( f . (n + 1) > g . (n + 1) or f . (n + 1) < g . (n + 1) ) by A10, XXREAL_0:1; caseA11: f . (n + 1) > g . (n + 1) ; ::_thesis: contradiction g . (n + 1) in rng f by A7, A9, FUNCT_1:def_3; then consider m being Nat such that A12: m in dom f and A13: f . m = g . (n + 1) by FINSEQ_2:10; A14: m <= len f by A12, FINSEQ_3:25; now__::_thesis:_(_(_m_=_len_f_&_contradiction_)_or_(_m_<>_len_f_&_contradiction_)_) percases ( m = len f or m <> len f ) ; case m = len f ; ::_thesis: contradiction hence contradiction by A1, A11, A13; ::_thesis: verum end; case m <> len f ; ::_thesis: contradiction then m < n + 1 by A1, A14, XXREAL_0:1; hence contradiction by A5, A11, A12, A13, Th19; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA15: f . (n + 1) < g . (n + 1) ; ::_thesis: contradiction f . (n + 1) in rng g by A5, A9, FUNCT_1:def_3; then consider m being Nat such that A16: m in dom g and A17: g . m = f . (n + 1) by FINSEQ_2:10; A18: m <= len g by A16, FINSEQ_3:25; now__::_thesis:_(_(_m_=_len_g_&_contradiction_)_or_(_m_<>_len_g_&_contradiction_)_) percases ( m = len g or m <> len g ) ; case m = len g ; ::_thesis: contradiction hence contradiction by A1, A2, A15, A17; ::_thesis: verum end; case m <> len g ; ::_thesis: contradiction then m < n + 1 by A1, A2, A18, XXREAL_0:1; hence contradiction by A7, A15, A16, A17, Th19; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence f . (len f) = g . (len g) by A1, A2; ::_thesis: f | n,g | n are_fiberwise_equipotent A19: g = (g | n) ^ <*(f . (n + 1))*> by A1, A2, A8, Th7; now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_((g_|_n),x)) let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim ((g | n),x)) (card (Coim ((f | n),x))) + (card (<*(f . (n + 1))*> " {x})) = card (Coim (f,x)) by A6, FINSEQ_3:57 .= card (Coim (g,x)) by A3, CLASSES1:def_9 .= (card (Coim ((g | n),x))) + (card (<*(f . (n + 1))*> " {x})) by A19, FINSEQ_3:57 ; hence card (Coim ((f | n),x)) = card (Coim ((g | n),x)) ; ::_thesis: verum end; hence f | n,g | n are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; defpred S2[ Nat] means for R being FinSequence of REAL st $1 = len R holds ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ; Lm5: S2[ 0 ] proof let R be FinSequence of REAL ; ::_thesis: ( 0 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ) assume len R = 0 ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent then reconsider a = R as non-increasing FinSequence of REAL by Th18; take a ; ::_thesis: R,a are_fiberwise_equipotent thus R,a are_fiberwise_equipotent ; ::_thesis: verum end; Lm6: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A1: S2[n] ; ::_thesis: S2[n + 1] let R be FinSequence of REAL ; ::_thesis: ( n + 1 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ) set fn = R | (Seg n); A2: R | (Seg n) = R | n by FINSEQ_1:def_15; set q = R . (n + 1); reconsider fn = R | (Seg n) as FinSequence by FINSEQ_1:15; rng fn c= rng R by RELAT_1:70; then rng fn c= REAL by XBOOLE_1:1; then reconsider fn = fn as FinSequence of REAL by FINSEQ_1:def_4; n <= n + 1 by NAT_1:11; then A3: ( dom fn = (dom R) /\ (Seg n) & Seg n c= Seg (n + 1) ) by FINSEQ_1:5, RELAT_1:61; assume A4: n + 1 = len R ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent then dom R = Seg (n + 1) by FINSEQ_1:def_3; then dom fn = Seg n by A3, XBOOLE_1:28; then A5: len fn = n by FINSEQ_1:def_3; then consider a being non-increasing FinSequence of REAL such that A6: fn,a are_fiberwise_equipotent by A1; A7: len fn = len a by A6, Th3; A8: Seg (len a) = dom a by FINSEQ_1:def_3; now__::_thesis:_(_(_(_for_t_being_Real_st_t_in_rng_a_holds_ R_._(n_+_1)_<=_t_)_&_ex_b_being_non-increasing_FinSequence_of_REAL_st_R,b_are_fiberwise_equipotent_)_or_(_ex_t_being_Real_st_ (_t_in_rng_a_&_not_R_._(n_+_1)_<=_t_)_&_ex_b_being_non-increasing_FinSequence_of_REAL_st_R,b_are_fiberwise_equipotent_)_) percases ( for t being Real st t in rng a holds R . (n + 1) <= t or ex t being Real st ( t in rng a & not R . (n + 1) <= t ) ) ; caseA9: for t being Real st t in rng a holds R . (n + 1) <= t ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent set b = a ^ <*(R . (n + 1))*>; A10: len (a ^ <*(R . (n + 1))*>) = n + (len <*(R . (n + 1))*>) by A5, A7, FINSEQ_1:22 .= n + 1 by FINSEQ_1:39 ; now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(a_^_<*(R_._(n_+_1))*>)_&_m_+_1_in_dom_(a_^_<*(R_._(n_+_1))*>)_holds_ (a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1) let m be Element of NAT ; ::_thesis: ( m in dom (a ^ <*(R . (n + 1))*>) & m + 1 in dom (a ^ <*(R . (n + 1))*>) implies (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) ) assume that A11: m in dom (a ^ <*(R . (n + 1))*>) and A12: m + 1 in dom (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) A13: 1 <= m + 1 by A12, FINSEQ_3:25; set r = (a ^ <*(R . (n + 1))*>) . m; set s = (a ^ <*(R . (n + 1))*>) . (m + 1); A14: 1 <= m by A11, FINSEQ_3:25; A15: m + 1 <= len (a ^ <*(R . (n + 1))*>) by A12, FINSEQ_3:25; then m <= (n + 1) - 1 by A10, XREAL_1:19; then m in Seg n by A14, FINSEQ_1:1; then A16: m in dom a by A5, A7, FINSEQ_1:def_3; then A17: (a ^ <*(R . (n + 1))*>) . m = a . m by FINSEQ_1:def_7; A18: a . m in rng a by A16, FUNCT_1:def_3; now__::_thesis:_(_(_m_+_1_=_len_(a_^_<*(R_._(n_+_1))*>)_&_(a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1)_)_or_(_m_+_1_<>_len_(a_^_<*(R_._(n_+_1))*>)_&_(a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1)_)_) percases ( m + 1 = len (a ^ <*(R . (n + 1))*>) or m + 1 <> len (a ^ <*(R . (n + 1))*>) ) ; case m + 1 = len (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) then (a ^ <*(R . (n + 1))*>) . (m + 1) = R . (n + 1) by A5, A7, A10, FINSEQ_1:42; hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A9, A17, A18; ::_thesis: verum end; case m + 1 <> len (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) then m + 1 < len (a ^ <*(R . (n + 1))*>) by A15, XXREAL_0:1; then m + 1 <= (n + 1) - 1 by A10, NAT_1:13; then m + 1 in Seg n by A13, FINSEQ_1:1; then A19: m + 1 in dom a by A5, A7, FINSEQ_1:def_3; then a . (m + 1) = (a ^ <*(R . (n + 1))*>) . (m + 1) by FINSEQ_1:def_7; hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A16, A17, A19, Def3; ::_thesis: verum end; end; end; hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) ; ::_thesis: verum end; then reconsider b = a ^ <*(R . (n + 1))*> as non-increasing FinSequence of REAL by Def3; take b = b; ::_thesis: R,b are_fiberwise_equipotent fn ^ <*(R . (n + 1))*> = R by A4, A2, Th7; hence R,b are_fiberwise_equipotent by A6, Th1; ::_thesis: verum end; caseA20: ex t being Real st ( t in rng a & not R . (n + 1) <= t ) ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent defpred S3[ Nat] means ( $1 in dom a & ( for r being Real st r = a . $1 holds r < R . (n + 1) ) ); A21: ex k being Nat st S3[k] proof consider t being Real such that A22: t in rng a and A23: t < R . (n + 1) by A20; consider k being Nat such that A24: k in dom a and A25: a . k = t by A22, FINSEQ_2:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: S3[k] thus k in dom a by A24; ::_thesis: for r being Real st r = a . k holds r < R . (n + 1) let r be Real; ::_thesis: ( r = a . k implies r < R . (n + 1) ) assume r = a . k ; ::_thesis: r < R . (n + 1) hence r < R . (n + 1) by A23, A25; ::_thesis: verum end; consider mi being Nat such that A26: ( S3[mi] & ( for m being Nat st S3[m] holds mi <= m ) ) from NAT_1:sch_5(A21); 1 <= mi by A26, FINSEQ_3:25; then max (0,(mi - 1)) = mi - 1 by FINSEQ_2:4; then reconsider k = mi - 1 as Element of NAT by FINSEQ_2:5; mi < mi + 1 by NAT_1:13; then A27: k <= mi by XREAL_1:19; A28: mi <= len a by A26, FINSEQ_3:25; then A29: k <= len a by A27, XXREAL_0:2; then A30: len (a /^ k) = (len a) - k by Def1; A31: dom ((a | k) ^ <*(R . (n + 1))*>) = Seg (len ((a | k) ^ <*(R . (n + 1))*>)) by FINSEQ_1:def_3; A32: dom (a | k) c= dom ((a | k) ^ <*(R . (n + 1))*>) by FINSEQ_1:26; set ak = a /^ k; set b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k); A33: dom (a | k) = Seg (len (a | k)) by FINSEQ_1:def_3; A34: len (a | k) = k by A28, A27, FINSEQ_1:59, XXREAL_0:2; then A35: len ((a | k) ^ <*(R . (n + 1))*>) = k + (len <*(R . (n + 1))*>) by FINSEQ_1:22 .= k + 1 by FINSEQ_1:39 ; then A36: len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) = (k + 1) + (len (a /^ k)) by FINSEQ_1:22; k + 1 <= len a by A26, FINSEQ_3:25; then A37: 1 <= len (a /^ k) by A30, XREAL_1:19; now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_&_m_+_1_in_dom_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_holds_ (((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1) let m be Element of NAT ; ::_thesis: ( m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) & m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) implies (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) assume that A38: m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) and A39: m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) A40: 1 <= m + 1 by A39, FINSEQ_3:25; A41: m + 1 <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A39, FINSEQ_3:25; set r = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m; set s = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1); A42: 1 <= m by A38, FINSEQ_3:25; A43: m <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A38, FINSEQ_3:25; now__::_thesis:_(_(_m_+_1_<=_k_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_<_m_+_1_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_) percases ( m + 1 <= k or k < m + 1 ) ; caseA44: m + 1 <= k ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) dom (a | k) c= dom ((a | k) ^ (a /^ k)) by FINSEQ_1:26; then A45: dom (a | k) c= dom a by Th8; A46: dom a = Seg (len a) by FINSEQ_1:def_3; m <= k by A44, NAT_1:13; then A47: m in Seg k by A42, FINSEQ_1:1; 1 <= k by A40, A44, XXREAL_0:2; then A48: k in dom a by A29, A46, FINSEQ_1:1; then A49: a . m = (a | k) . m by A47, Th6; A50: m + 1 in Seg k by A40, A44, FINSEQ_1:1; then A51: a . (m + 1) = (a | k) . (m + 1) by A48, Th6; A52: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (m + 1) by A34, A33, A32, A50, FINSEQ_1:def_7 .= a . (m + 1) by A34, A33, A50, A51, FINSEQ_1:def_7 ; (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A47, FINSEQ_1:def_7 .= a . m by A34, A33, A47, A49, FINSEQ_1:def_7 ; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A34, A33, A47, A50, A52, A45, Def3; ::_thesis: verum end; case k < m + 1 ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) then A53: k <= m by NAT_1:13; now__::_thesis:_(_(_k_=_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_<>_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_) percases ( k = m or k <> m ) ; caseA54: k = m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) then m + 1 in dom ((a | k) ^ <*(R . (n + 1))*>) by A35, A31, FINSEQ_1:4; then A55: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A54, FINSEQ_1:def_7 .= R . (n + 1) by A34, FINSEQ_1:42 ; A56: m in Seg k by A42, A54, FINSEQ_1:1; A57: k in dom a by A8, A29, A42, A54, FINSEQ_1:1; then A58: a . m = (a | k) . m by A56, Th6; A59: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A56, FINSEQ_1:def_7 .= a . m by A34, A33, A56, A58, FINSEQ_1:def_7 ; now__::_thesis:_not_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_>_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m assume (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) > (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m ; ::_thesis: contradiction then for t being Real st t = a . k holds t < R . (n + 1) by A54, A59, A55; then mi <= k by A26, A57; hence contradiction by XREAL_1:44; ::_thesis: verum end; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum end; case k <> m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) then k < m by A53, XXREAL_0:1; then A60: k + 1 <= m by NAT_1:13; then A61: k + 1 < m + 1 by NAT_1:13; max (0,(m - (k + 1))) = m - (k + 1) by A60, FINSEQ_2:4; then reconsider l = m - (k + 1) as Element of NAT by FINSEQ_2:5; A62: l + 1 = (m + 1) - (k + 1) ; then A63: l + 1 <= (len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k))) - (k + 1) by A41, XREAL_1:13; l <= l + 1 by NAT_1:11; then A64: l <= len (a /^ k) by A36, A63, XXREAL_0:2; 1 <= l + 1 by NAT_1:11; then A65: l + 1 in dom (a /^ k) by A36, A63, FINSEQ_3:25; 1 <= (l + 1) + k by A38, FINSEQ_3:25; then A66: (k + l) + 1 <= len a by A30, A36, A63, XREAL_1:19; then A67: (k + l) + 1 in dom a by A42, FINSEQ_3:25; k + l <= (k + l) + 1 by NAT_1:11; then A68: k + l <= len a by A66, XXREAL_0:2; A69: k + (l + 1) <= len a by A30, A36, A63, XREAL_1:19; now__::_thesis:_(_(_k_+_1_=_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_+_1_<>_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_) percases ( k + 1 = m or k + 1 <> m ) ; caseA70: k + 1 = m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) then m in Seg (k + 1) by A42, FINSEQ_1:1; then A71: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A35, A31, A70, FINSEQ_1:def_7 .= R . (n + 1) by A34, FINSEQ_1:42 ; A72: 1 in dom (a /^ k) by A37, FINSEQ_3:25; (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (((k + 1) + 1) - (k + 1)) by A35, A41, A61, A70, FINSEQ_1:24 .= a . mi by A29, A72, Def1 ; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A26, A71; ::_thesis: verum end; case k + 1 <> m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) then A73: k + 1 < m by A60, XXREAL_0:1; then (k + 1) + 1 <= m by NAT_1:13; then A74: 1 <= l by XREAL_1:19; then A75: l in dom (a /^ k) by A64, FINSEQ_3:25; l <= k + l by NAT_1:11; then 1 <= k + l by A74, XXREAL_0:2; then A76: k + l in dom a by A68, FINSEQ_3:25; A77: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = (a /^ k) . l by A35, A43, A73, FINSEQ_1:24 .= a . (k + l) by A29, A75, Def1 ; (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (l + 1) by A35, A41, A61, A62, FINSEQ_1:24 .= a . ((k + l) + 1) by A29, A65, A69, Def1 ; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A67, A77, A76, Def3; ::_thesis: verum end; end; end; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum end; end; end; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum end; end; end; hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum end; then reconsider b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k) as non-increasing FinSequence of REAL by Def3; take b = b; ::_thesis: R,b are_fiberwise_equipotent now__::_thesis:_for_x_being_set_holds_card_(Coim_(b,x))_=_card_(Coim_(R,x)) let x be set ; ::_thesis: card (Coim (b,x)) = card (Coim (R,x)) A78: card (Coim (fn,x)) = card (Coim (a,x)) by A6, CLASSES1:def_9; thus card (Coim (b,x)) = (card (((a | k) ^ <*(R . (n + 1))*>) " {x})) + (card ((a /^ k) " {x})) by FINSEQ_3:57 .= ((card ((a | k) " {x})) + (card (<*(R . (n + 1))*> " {x}))) + (card ((a /^ k) " {x})) by FINSEQ_3:57 .= ((card ((a | k) " {x})) + (card ((a /^ k) " {x}))) + (card (<*(R . (n + 1))*> " {x})) .= (card (((a | k) ^ (a /^ k)) " {x})) + (card (<*(R . (n + 1))*> " {x})) by FINSEQ_3:57 .= (card (fn " {x})) + (card (<*(R . (n + 1))*> " {x})) by A78, Th8 .= card ((fn ^ <*(R . (n + 1))*>) " {x}) by FINSEQ_3:57 .= card (Coim (R,x)) by A4, A2, Th7 ; ::_thesis: verum end; hence R,b are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; end; end; hence ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ; ::_thesis: verum end; theorem Th22: :: RFINSEQ:22 for R being FinSequence of REAL ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent proof let R be FinSequence of REAL ; ::_thesis: ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent A1: len R = len R ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(Lm5, Lm6); hence ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent by A1; ::_thesis: verum end; Lm7: for n being Element of NAT for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2 proof defpred S3[ Nat] means for g1, g2 being non-increasing FinSequence of REAL st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2; A1: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume A2: S3[n] ; ::_thesis: S3[n + 1] let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( n + 1 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 ) set r = g1 . (n + 1); reconsider g1n = g1 | n, g2n = g2 | n as non-increasing FinSequence of REAL by Th20; assume that A3: len g1 = n + 1 and A4: g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2 A5: len g2 = len g1 by A4, Th3; then A6: g1 . (len g1) = g2 . (len g2) by A3, A4, Lm4; A7: (g1 | n) ^ <*(g1 . (n + 1))*> = g1 by A3, Th7; len (g1 | n) = n by A3, FINSEQ_1:59, NAT_1:11; then g1n = g2n by A2, A3, A4, A5, Lm4; hence g1 = g2 by A3, A5, A6, A7, Th7; ::_thesis: verum end; A8: S3[ 0 ] proof let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( 0 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 ) assume ( len g1 = 0 & g1,g2 are_fiberwise_equipotent ) ; ::_thesis: g1 = g2 then ( len g2 = len g1 & g1 = <*> REAL ) by Th3; hence g1 = g2 ; ::_thesis: verum end; thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A8, A1); ::_thesis: verum end; theorem :: RFINSEQ:23 for R1, R2 being non-increasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds R1 = R2 proof let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 ) A1: len g1 = len g1 ; assume g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2 hence g1 = g2 by A1, Lm7; ::_thesis: verum end; theorem :: RFINSEQ:24 for R being FinSequence of REAL for r, s being Real st r <> 0 holds R " {(s / r)} = (r * R) " {s} proof let R be FinSequence of REAL ; ::_thesis: for r, s being Real st r <> 0 holds R " {(s / r)} = (r * R) " {s} let r, s be Real; ::_thesis: ( r <> 0 implies R " {(s / r)} = (r * R) " {s} ) A1: ( Seg (len R) = dom R & dom (r * R) = Seg (len (r * R)) ) by FINSEQ_1:def_3; assume A2: r <> 0 ; ::_thesis: R " {(s / r)} = (r * R) " {s} thus R " {(s / r)} c= (r * R) " {s} :: according to XBOOLE_0:def_10 ::_thesis: (r * R) " {s} c= R " {(s / r)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " {(s / r)} or x in (r * R) " {s} ) assume A3: x in R " {(s / r)} ; ::_thesis: x in (r * R) " {s} then reconsider i = x as Element of NAT ; R . i in {(s / r)} by A3, FUNCT_1:def_7; then R . i = s / r by TARSKI:def_1; then r * (R . i) = s by A2, XCMPLX_1:87; then (r * R) . i = s by RVSUM_1:44; then A4: (r * R) . i in {s} by TARSKI:def_1; i in dom R by A3, FUNCT_1:def_7; then i in dom (r * R) by A1, FINSEQ_2:33; hence x in (r * R) " {s} by A4, FUNCT_1:def_7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (r * R) " {s} or x in R " {(s / r)} ) assume A5: x in (r * R) " {s} ; ::_thesis: x in R " {(s / r)} then reconsider i = x as Element of NAT ; (r * R) . i in {s} by A5, FUNCT_1:def_7; then (r * R) . i = s by TARSKI:def_1; then r * (R . i) = s by RVSUM_1:44; then R . i = s / r by A2, XCMPLX_1:89; then A6: R . i in {(s / r)} by TARSKI:def_1; i in dom (r * R) by A5, FUNCT_1:def_7; then i in dom R by A1, FINSEQ_2:33; hence x in R " {(s / r)} by A6, FUNCT_1:def_7; ::_thesis: verum end; theorem :: RFINSEQ:25 for R being FinSequence of REAL holds (0 * R) " {0} = dom R proof let R be FinSequence of REAL ; ::_thesis: (0 * R) " {0} = dom R A1: Seg (len (0 * R)) = dom (0 * R) by FINSEQ_1:def_3; A2: ( len (0 * R) = len R & dom R = Seg (len R) ) by FINSEQ_1:def_3, FINSEQ_2:33; hence (0 * R) " {0} c= dom R by A1, RELAT_1:132; :: according to XBOOLE_0:def_10 ::_thesis: dom R c= (0 * R) " {0} let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in (0 * R) " {0} ) assume A3: x in dom R ; ::_thesis: x in (0 * R) " {0} then reconsider i = x as Element of NAT ; (0 * R) . i = 0 * (R . i) by RVSUM_1:44 .= 0 ; then (0 * R) . i in {0} by TARSKI:def_1; hence x in (0 * R) " {0} by A2, A1, A3, FUNCT_1:def_7; ::_thesis: verum end; begin theorem :: RFINSEQ:26 for f, g being Function st rng f = rng g & f is one-to-one & g is one-to-one holds f,g are_fiberwise_equipotent proof let f, g be Function; ::_thesis: ( rng f = rng g & f is one-to-one & g is one-to-one implies f,g are_fiberwise_equipotent ) assume that A1: rng f = rng g and A2: f is one-to-one and A3: g is one-to-one ; ::_thesis: f,g are_fiberwise_equipotent let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim (f,x)) = card (Coim (g,x)) percases ( x in rng f or not x in rng f ) ; supposeA4: x in rng f ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x)) then card (Coim (f,x)) = 1 by A2, FINSEQ_4:73; hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A3, A4, FINSEQ_4:73; ::_thesis: verum end; supposeA5: not x in rng f ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x)) then card (f " {x}) = 0 by CARD_1:27, FUNCT_1:72; hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A5, CARD_1:27, FUNCT_1:72; ::_thesis: verum end; end; end; theorem :: RFINSEQ:27 for D being set for f being FinSequence of D holds f /^ (len f) = {} proof let D be set ; ::_thesis: for f being FinSequence of D holds f /^ (len f) = {} let f be FinSequence of D; ::_thesis: f /^ (len f) = {} len (f /^ (len f)) = (len f) - (len f) by Def1 .= 0 ; hence f /^ (len f) = {} ; ::_thesis: verum end; theorem :: RFINSEQ:28 for f, g being Function for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds f . k = g . k ) holds f,g are_fiberwise_equipotent proof let f, g be Function; ::_thesis: for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds f . k = g . k ) holds f,g are_fiberwise_equipotent let m, n be set ; ::_thesis: ( f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds f . k = g . k ) implies f,g are_fiberwise_equipotent ) assume that A1: f . m = g . n and A2: f . n = g . m and A3: m in dom f and A4: n in dom f and A5: dom f = dom g and A6: for k being set st k <> m & k <> n & k in dom f holds f . k = g . k ; ::_thesis: f,g are_fiberwise_equipotent set t = id (dom f); set nm = n .--> m; set mn = m .--> n; set p = ((id (dom f)) +* (n .--> m)) +* (m .--> n); A7: dom (n .--> m) = {n} by FUNCOP_1:13; A8: dom (id (dom f)) = dom f ; A9: rng (id (dom f)) = dom ((id (dom f)) ") by FUNCT_1:33 .= dom f by A8, FUNCT_1:45 ; dom (m .--> n) = {m} by FUNCOP_1:13; then A10: dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = (dom ((id (dom f)) +* (n .--> m))) \/ {m} by FUNCT_4:def_1 .= ((dom (id (dom f))) \/ {n}) \/ {m} by A7, FUNCT_4:def_1 .= ((dom f) \/ {n}) \/ {m} .= (dom f) \/ {m} by A4, ZFMISC_1:40 .= dom f by A3, ZFMISC_1:40 ; A11: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ ((((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n))_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_x let x be set ; ::_thesis: ( x in dom f implies ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 ) assume A12: x in dom f ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 then A13: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A10, FUNCT_1:13; percases ( x = m or x <> m ) ; supposeA14: x = m ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . n by A13, FUNCT_4:89 .= x by A14, FUNCT_4:90 ; ::_thesis: verum end; supposeA15: x <> m ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 now__::_thesis:_((((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n))_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_x percases ( x = n or x <> n ) ; supposeA16: x = n ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . m by A13, FUNCT_4:90 .= x by A16, FUNCT_4:89 ; ::_thesis: verum end; supposeA17: x <> n ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((id (dom f)) . x) by A13, A15, FUNCT_4:91 .= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by A12, FUNCT_1:17 .= (id (dom f)) . x by A15, A17, FUNCT_4:91 .= x by A12, FUNCT_1:17 ; ::_thesis: verum end; end; end; hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x ; ::_thesis: verum end; end; end; rng (n .--> m) = {m} by FUNCOP_1:8; then (rng (id (dom f))) \/ (rng (n .--> m)) = dom f by A3, ZFMISC_1:40; then A18: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by FUNCT_4:17, XBOOLE_1:9; for z being set st z in rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) holds z in rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by FUNCT_1:14; then A19: rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) c= rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by TARSKI:def_3; A20: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) by FUNCT_4:17; A21: rng (m .--> n) = {n} by FUNCOP_1:8; then (dom f) \/ (rng (m .--> n)) = dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, ZFMISC_1:40; then A22: dom ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A10, A18, A20, RELAT_1:27, XBOOLE_1:1; then (((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = id (dom f) by A11, FUNCT_1:17; then A23: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by A10, FUNCT_1:31; rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by A18, A20, XBOOLE_1:1; then A24: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, A21, ZFMISC_1:40; then A25: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A5, A10, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (g_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_f_._x let x be set ; ::_thesis: ( x in dom f implies (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 ) assume A26: x in dom f ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 then A27: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A25, FUNCT_1:12; percases ( x = m or x <> m ) ; suppose x = m ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A1, A27, FUNCT_4:89; ::_thesis: verum end; supposeA28: x <> m ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 now__::_thesis:_(g_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_f_._x percases ( x = n or x <> n ) ; suppose x = n ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A2, A27, FUNCT_4:90; ::_thesis: verum end; supposeA29: x <> n ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((id (dom f)) . x) by A27, A28, FUNCT_4:91 .= g . x by A26, FUNCT_1:17 .= f . x by A6, A26, A28, A29 ; ::_thesis: verum end; end; end; hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x ; ::_thesis: verum end; end; end; then A30: f = g * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A25, FUNCT_1:2; rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A9, A22, A11, FUNCT_1:17; then rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A10, A24, A19, XBOOLE_0:def_10; hence f,g are_fiberwise_equipotent by A10, A23, A30, CLASSES1:77; ::_thesis: verum end; theorem :: RFINSEQ:29 for D being non empty set for f being FinSequence of D for k being Nat holds len (f /^ k) = (len f) -' k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k being Nat holds len (f /^ k) = (len f) -' k let f be FinSequence of D; ::_thesis: for k being Nat holds len (f /^ k) = (len f) -' k let k be Nat; ::_thesis: len (f /^ k) = (len f) -' k percases ( k <= len f or k > len f ) ; supposeA1: k <= len f ; ::_thesis: len (f /^ k) = (len f) -' k then (len f) -' k = (len f) - k by XREAL_1:233; hence len (f /^ k) = (len f) -' k by A1, Def1; ::_thesis: verum end; supposeA2: k > len f ; ::_thesis: len (f /^ k) = (len f) -' k then f /^ k = <*> D by Def1; then A3: len (f /^ k) = 0 ; (len f) - k < 0 by A2, XREAL_1:49; hence len (f /^ k) = (len f) -' k by A3, XREAL_0:def_2; ::_thesis: verum end; end; end; theorem Th30: :: RFINSEQ:30 for f, g being FinSequence for x being set st x in dom g & f,g are_fiberwise_equipotent holds ex y being set st ( y in dom g & f . x = g . y ) proof let f, g be FinSequence; ::_thesis: for x being set st x in dom g & f,g are_fiberwise_equipotent holds ex y being set st ( y in dom g & f . x = g . y ) let x be set ; ::_thesis: ( x in dom g & f,g are_fiberwise_equipotent implies ex y being set st ( y in dom g & f . x = g . y ) ) assume that A1: x in dom g and A2: f,g are_fiberwise_equipotent ; ::_thesis: ex y being set st ( y in dom g & f . x = g . y ) consider P being Permutation of (dom g) such that A3: f = g * P by A2, Th4; take y = P . x; ::_thesis: ( y in dom g & f . x = g . y ) thus y in dom g by A1, FUNCT_2:5; ::_thesis: f . x = g . y thus f . x = g . y by A1, A3, FUNCT_2:15; ::_thesis: verum end; theorem Th31: :: RFINSEQ:31 for f, g, h being FinSequence holds ( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent ) proof let f, g, h be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent ) thus ( f,g are_fiberwise_equipotent implies h ^ f,h ^ g are_fiberwise_equipotent ) ::_thesis: ( h ^ f,h ^ g are_fiberwise_equipotent implies f,g are_fiberwise_equipotent ) proof assume A1: f,g are_fiberwise_equipotent ; ::_thesis: h ^ f,h ^ g are_fiberwise_equipotent now__::_thesis:_for_y_being_set_holds_card_(Coim_((h_^_f),y))_=_card_(Coim_((h_^_g),y)) let y be set ; ::_thesis: card (Coim ((h ^ f),y)) = card (Coim ((h ^ g),y)) card (Coim (f,y)) = card (Coim (g,y)) by A1, CLASSES1:def_9; hence card (Coim ((h ^ f),y)) = (card (g " {y})) + (card (h " {y})) by FINSEQ_3:57 .= card (Coim ((h ^ g),y)) by FINSEQ_3:57 ; ::_thesis: verum end; hence h ^ f,h ^ g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; assume A2: h ^ f,h ^ g are_fiberwise_equipotent ; ::_thesis: f,g are_fiberwise_equipotent now__::_thesis:_for_x_being_set_holds_card_(Coim_(f,x))_=_card_(Coim_(g,x)) let x be set ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x)) A3: ( card (Coim ((h ^ f),x)) = (card (Coim (f,x))) + (card (h " {x})) & card ((h ^ g) " {x}) = (card (g " {x})) + (card (h " {x})) ) by FINSEQ_3:57; card (Coim ((h ^ f),x)) = card (Coim ((h ^ g),x)) by A2, CLASSES1:def_9; hence card (Coim (f,x)) = card (Coim (g,x)) by A3; ::_thesis: verum end; hence f,g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; theorem :: RFINSEQ:32 for f, g being FinSequence for m, n, j being Element of NAT st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds f . i = g . i ) & m < j & j <= n holds ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) proof let f, g be FinSequence; ::_thesis: for m, n, j being Element of NAT st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds f . i = g . i ) & m < j & j <= n holds ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) let m, n, j be Element of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds f . i = g . i ) & m < j & j <= n implies ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) ) assume A1: f,g are_fiberwise_equipotent ; ::_thesis: ( not m <= n or not n <= len f or ex i being Element of NAT st ( 1 <= i & i <= m & not f . i = g . i ) or ex i being Element of NAT st ( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) ) assume that A2: m <= n and A3: n <= len f ; ::_thesis: ( ex i being Element of NAT st ( 1 <= i & i <= m & not f . i = g . i ) or ex i being Element of NAT st ( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) ) assume A4: for i being Element of NAT st 1 <= i & i <= m holds f . i = g . i ; ::_thesis: ( ex i being Element of NAT st ( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) ) reconsider m3 = (len f) - n as Element of NAT by A3, INT_1:3, XREAL_1:48; len g = n + m3 by A1, Th3; then consider s2, r2 being FinSequence such that A5: len s2 = n and A6: len r2 = m3 and A7: g = s2 ^ r2 by FINSEQ_2:22; A8: len f = n + m3 ; then consider s1, r1 being FinSequence such that A9: len s1 = n and A10: len r1 = m3 and A11: f = s1 ^ r1 by FINSEQ_2:22; A12: dom r1 = Seg m3 by A10, FINSEQ_1:def_3; assume A13: for i being Element of NAT st n < i & i <= len f holds f . i = g . i ; ::_thesis: ( not m < j or not j <= n or ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) ) now__::_thesis:_for_i_being_Nat_st_i_in_dom_r1_holds_ r1_._i_=_r2_._i let i be Nat; ::_thesis: ( i in dom r1 implies r1 . i = r2 . i ) reconsider a = i as Element of NAT by ORDINAL1:def_12; A14: n < n + 1 by XREAL_1:29; assume A15: i in dom r1 ; ::_thesis: r1 . i = r2 . i then A16: i in dom r2 by A6, A12, FINSEQ_1:def_3; 1 <= i by A12, A15, FINSEQ_1:1; then n + 1 <= n + i by XREAL_1:6; then A17: n < i + n by A14, XXREAL_0:2; i <= m3 by A12, A15, FINSEQ_1:1; then A18: (len s1) + i <= len f by A8, A9, XREAL_1:6; thus r1 . i = f . ((len s1) + i) by A11, A15, FINSEQ_1:def_7 .= g . ((len s2) + a) by A13, A9, A5, A17, A18 .= r2 . i by A7, A16, FINSEQ_1:def_7 ; ::_thesis: verum end; then r1 = r2 by A10, A6, FINSEQ_2:9; then A19: s1,s2 are_fiberwise_equipotent by A1, A11, A7, Th1; reconsider m2 = n - m as Element of NAT by A2, INT_1:3, XREAL_1:48; A20: m + 1 > m by XREAL_1:29; len s2 = m + m2 by A5; then consider p2, q2 being FinSequence such that A21: len p2 = m and A22: len q2 = m2 and A23: s2 = p2 ^ q2 by FINSEQ_2:22; A24: Seg m = dom p2 by A21, FINSEQ_1:def_3; len s1 = m + m2 by A9; then consider p1, q1 being FinSequence such that A25: len p1 = m and A26: len q1 = m2 and A27: s1 = p1 ^ q1 by FINSEQ_2:22; A28: f = p1 ^ (q1 ^ r1) by A11, A27, FINSEQ_1:32; A29: dom p1 = Seg m by A25, FINSEQ_1:def_3; A30: g = p2 ^ (q2 ^ r2) by A7, A23, FINSEQ_1:32; now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_ p1_._i_=_p2_._i let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i ) reconsider a = i as Element of NAT by ORDINAL1:def_12; assume A31: i in dom p1 ; ::_thesis: p1 . i = p2 . i then A32: ( 1 <= i & i <= m ) by A29, FINSEQ_1:1; thus p1 . i = f . i by A28, A31, FINSEQ_1:def_7 .= g . a by A4, A32 .= p2 . i by A30, A24, A29, A31, FINSEQ_1:def_7 ; ::_thesis: verum end; then p1 = p2 by A25, A21, FINSEQ_2:9; then A33: q1,q2 are_fiberwise_equipotent by A27, A23, A19, Th31; assume that A34: m < j and A35: j <= n ; ::_thesis: ex k being Element of NAT st ( m < k & k <= n & f . j = g . k ) j - (len p1) > 0 by A34, A25, XREAL_1:50; then reconsider x = j - (len p1) as Element of NAT by INT_1:3; A36: x <= n - (len p1) by A35, XREAL_1:9; A37: Seg m2 = dom q2 by A22, FINSEQ_1:def_3; A38: 1 + 0 <= x by A34, A25, INT_1:7, XREAL_1:50; then x in dom q2 by A25, A37, A36, FINSEQ_1:1; then consider y being set such that A39: y in dom q2 and A40: q1 . x = q2 . y by A33, Th30; reconsider y = y as Element of NAT by A39; A41: (len p2) + y in dom s2 by A23, A39, FINSEQ_1:28; reconsider k = (len p2) + y as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( m < k & k <= n & f . j = g . k ) 1 <= y by A37, A39, FINSEQ_1:1; then k >= (len p2) + 1 by XREAL_1:6; hence m < k by A21, A20, XXREAL_0:2; ::_thesis: ( k <= n & f . j = g . k ) y <= m2 by A37, A39, FINSEQ_1:1; then k <= m2 + (len p2) by XREAL_1:6; hence k <= n by A21; ::_thesis: f . j = g . k Seg m2 = dom q1 by A26, FINSEQ_1:def_3; then A42: x in dom q1 by A25, A38, A36, FINSEQ_1:1; then (len p1) + x in dom s1 by A27, FINSEQ_1:28; hence f . j = s1 . ((len p1) + x) by A11, FINSEQ_1:def_7 .= q2 . y by A27, A40, A42, FINSEQ_1:def_7 .= s2 . ((len p2) + y) by A23, A39, FINSEQ_1:def_7 .= g . k by A7, A41, FINSEQ_1:def_7 ; ::_thesis: verum end; theorem :: RFINSEQ:33 for t being FinSequence of INT ex u being FinSequence of REAL st ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing ) proof let t be FinSequence of INT ; ::_thesis: ex u being FinSequence of REAL st ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing ) t is FinSequence of REAL by FINSEQ_3:117; then consider u being non-increasing FinSequence of REAL such that A1: t,u are_fiberwise_equipotent by Th22; take u ; ::_thesis: ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing ) thus t,u are_fiberwise_equipotent by A1; ::_thesis: ( u is FinSequence of INT & u is non-increasing ) rng t = rng u by A1, CLASSES1:75; hence u is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: u is non-increasing thus u is non-increasing ; ::_thesis: verum end;