:: FINSEQ_6 semantic presentation begin registration let x, y, z be set ; cluster<*x,y,z*> -> non trivial ; coherence not <*x,y,z*> is trivial proof len <*x,y,z*> = 3 by FINSEQ_1:45; hence not <*x,y,z*> is trivial by NAT_D:60; ::_thesis: verum end; end; registration let f be non empty FinSequence; cluster Rev f -> non empty ; coherence not Rev f is empty proof dom f <> {} ; hence not Rev f is empty by FINSEQ_5:57, RELAT_1:38; ::_thesis: verum end; end; Lm1: for x, y being set holds rng <*x,y*> = {x,y} proof let x, y be set ; ::_thesis: rng <*x,y*> = {x,y} <*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def_9; hence rng <*x,y*> = (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:31 .= {x} \/ (rng <*y*>) by FINSEQ_1:38 .= {x} \/ {y} by FINSEQ_1:38 .= {x,y} by ENUMSET1:1 ; ::_thesis: verum end; Lm2: for x, y, z being set holds rng <*x,y,z*> = {x,y,z} proof let x, y, z be set ; ::_thesis: rng <*x,y,z*> = {x,y,z} <*x,y,z*> = <*x,y*> ^ <*z*> by FINSEQ_1:43; hence rng <*x,y,z*> = (rng <*x,y*>) \/ (rng <*z*>) by FINSEQ_1:31 .= {x,y} \/ (rng <*z*>) by Lm1 .= {x,y} \/ {z} by FINSEQ_1:38 .= {x,y,z} by ENUMSET1:3 ; ::_thesis: verum end; begin theorem Th1: :: FINSEQ_6:1 for X being set for i being Nat st X c= Seg i & 1 in X holds (Sgm X) . 1 = 1 proof let X be set ; ::_thesis: for i being Nat st X c= Seg i & 1 in X holds (Sgm X) . 1 = 1 let i be Nat; ::_thesis: ( X c= Seg i & 1 in X implies (Sgm X) . 1 = 1 ) assume that A1: X c= Seg i and A2: 1 in X ; ::_thesis: (Sgm X) . 1 = 1 Sgm X <> {} by A1, A2, FINSEQ_1:51; then len (Sgm X) >= 1 by NAT_1:14; then 1 in dom (Sgm X) by FINSEQ_3:25; then A3: (Sgm X) . 1 in rng (Sgm X) by FUNCT_1:def_3; rng (Sgm X) c= NAT by FINSEQ_1:def_4; then reconsider k1 = (Sgm X) . 1 as Element of NAT by A3; assume A4: (Sgm X) . 1 <> 1 ; ::_thesis: contradiction A5: rng (Sgm X) = X by A1, FINSEQ_1:def_13; then consider x being set such that A6: x in dom (Sgm X) and A7: (Sgm X) . x = 1 by A2, FUNCT_1:def_3; A8: k1 >= 1 by A1, A5, A3, FINSEQ_1:1; reconsider j = x as Element of NAT by A6; j >= 1 by A6, FINSEQ_3:25; then A9: 1 < j by A7, A4, XXREAL_0:1; j <= len (Sgm X) by A6, FINSEQ_3:25; hence contradiction by A1, A7, A8, A9, FINSEQ_1:def_13; ::_thesis: verum end; theorem Th2: :: FINSEQ_6:2 for k being Nat for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds f . i <> f . k ) holds (f . k) .. f = k proof let k be Nat; ::_thesis: for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds f . i <> f . k ) holds (f . k) .. f = k let f be FinSequence; ::_thesis: ( k in dom f & ( for i being Nat st 1 <= i & i < k holds f . i <> f . k ) implies (f . k) .. f = k ) assume that A1: k in dom f and A2: for i being Nat st 1 <= i & i < k holds f . i <> f . k ; ::_thesis: (f . k) .. f = k assume A3: (f . k) .. f <> k ; ::_thesis: contradiction (f . k) .. f <= k by A1, FINSEQ_4:24; then A4: (f . k) .. f < k by A3, XXREAL_0:1; A5: f . k in rng f by A1, FUNCT_1:def_3; then f . ((f . k) .. f) = f . k by FINSEQ_4:19; hence contradiction by A2, A5, A4, FINSEQ_4:21; ::_thesis: verum end; theorem Th3: :: FINSEQ_6:3 for p1, p2 being set holds <*p1,p2*> | (Seg 1) = <*p1*> proof let p1, p2 be set ; ::_thesis: <*p1,p2*> | (Seg 1) = <*p1*> set f = <*p1,p2*> | (Seg 1); len <*p1,p2*> = 2 by FINSEQ_1:44; then 1 in dom <*p1,p2*> by FINSEQ_3:25; then A1: Seg 1 c= dom <*p1,p2*> by FINSEQ_1:2, ZFMISC_1:31; A2: dom (<*p1,p2*> | (Seg 1)) = (dom <*p1,p2*>) /\ (Seg 1) by RELAT_1:61 .= Seg 1 by A1, XBOOLE_1:28 ; then reconsider f = <*p1,p2*> | (Seg 1) as FinSequence by FINSEQ_1:def_2; 1 in dom f by A2, FINSEQ_1:2, TARSKI:def_1; then A3: f . 1 = <*p1,p2*> . 1 by FUNCT_1:47 .= p1 by FINSEQ_1:44 ; len f = 1 by A2, FINSEQ_1:def_3; hence <*p1,p2*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:40; ::_thesis: verum end; theorem Th4: :: FINSEQ_6:4 for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 1) = <*p1*> proof let p1, p2, p3 be set ; ::_thesis: <*p1,p2,p3*> | (Seg 1) = <*p1*> set f = <*p1,p2,p3*> | (Seg 1); len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then 1 in dom <*p1,p2,p3*> by FINSEQ_3:25; then A1: Seg 1 c= dom <*p1,p2,p3*> by FINSEQ_1:2, ZFMISC_1:31; A2: dom (<*p1,p2,p3*> | (Seg 1)) = (dom <*p1,p2,p3*>) /\ (Seg 1) by RELAT_1:61 .= Seg 1 by A1, XBOOLE_1:28 ; then reconsider f = <*p1,p2,p3*> | (Seg 1) as FinSequence by FINSEQ_1:def_2; 1 in dom f by A2, FINSEQ_1:2, TARSKI:def_1; then A3: f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47 .= p1 by FINSEQ_1:45 ; len f = 1 by A2, FINSEQ_1:def_3; hence <*p1,p2,p3*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:40; ::_thesis: verum end; theorem Th5: :: FINSEQ_6:5 for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> proof let p1, p2, p3 be set ; ::_thesis: <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> set f = <*p1,p2,p3*> | (Seg 2); A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then A2: 2 in dom <*p1,p2,p3*> by FINSEQ_3:25; 1 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25; then A3: Seg 2 c= dom <*p1,p2,p3*> by A2, FINSEQ_1:2, ZFMISC_1:32; A4: dom (<*p1,p2,p3*> | (Seg 2)) = (dom <*p1,p2,p3*>) /\ (Seg 2) by RELAT_1:61 .= Seg 2 by A3, XBOOLE_1:28 ; then reconsider f = <*p1,p2,p3*> | (Seg 2) as FinSequence by FINSEQ_1:def_2; A5: len f = 2 by A4, FINSEQ_1:def_3; then 2 in dom f by FINSEQ_3:25; then A6: f . 2 = <*p1,p2,p3*> . 2 by FUNCT_1:47 .= p2 by FINSEQ_1:45 ; 1 in dom f by A5, FINSEQ_3:25; then f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47 .= p1 by FINSEQ_1:45 ; hence <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> by A5, A6, FINSEQ_1:44; ::_thesis: verum end; theorem Th6: :: FINSEQ_6:6 for f1, f2 being FinSequence for p being set st p in rng f1 holds p .. (f1 ^ f2) = p .. f1 proof let f1, f2 be FinSequence; ::_thesis: for p being set st p in rng f1 holds p .. (f1 ^ f2) = p .. f1 let p be set ; ::_thesis: ( p in rng f1 implies p .. (f1 ^ f2) = p .. f1 ) A1: dom f1 c= dom (f1 ^ f2) by FINSEQ_1:26; assume A2: p in rng f1 ; ::_thesis: p .. (f1 ^ f2) = p .. f1 then A3: p .. f1 in dom f1 by FINSEQ_4:20; A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_p_.._f1_holds_ (f1_^_f2)_._i_<>_(f1_^_f2)_._(p_.._f1) A5: (f1 ^ f2) . (p .. f1) = f1 . (p .. f1) by A3, FINSEQ_1:def_7; let i be Nat; ::_thesis: ( 1 <= i & i < p .. f1 implies (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) ) assume that A6: 1 <= i and A7: i < p .. f1 ; ::_thesis: (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) p .. f1 <= len f1 by A2, FINSEQ_4:21; then i <= len f1 by A7, XXREAL_0:2; then A8: i in dom f1 by A6, FINSEQ_3:25; then (f1 ^ f2) . i = f1 . i by FINSEQ_1:def_7; hence (f1 ^ f2) . i <> (f1 ^ f2) . (p .. f1) by A2, A7, A8, A5, FINSEQ_4:19, FINSEQ_4:24; ::_thesis: verum end; f1 . (p .. f1) = p by A2, FINSEQ_4:19; then (f1 ^ f2) . (p .. f1) = p by A3, FINSEQ_1:def_7; hence p .. (f1 ^ f2) = p .. f1 by A3, A1, A4, Th2; ::_thesis: verum end; theorem Th7: :: FINSEQ_6:7 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds p .. (f1 ^ f2) = (len f1) + (p .. f2) proof let f2, f1 be FinSequence; ::_thesis: for p being set st p in (rng f2) \ (rng f1) holds p .. (f1 ^ f2) = (len f1) + (p .. f2) let p be set ; ::_thesis: ( p in (rng f2) \ (rng f1) implies p .. (f1 ^ f2) = (len f1) + (p .. f2) ) assume A1: p in (rng f2) \ (rng f1) ; ::_thesis: p .. (f1 ^ f2) = (len f1) + (p .. f2) then A2: p .. f2 in dom f2 by FINSEQ_4:20; f2 . (p .. f2) = p by A1, FINSEQ_4:19; then A3: (f1 ^ f2) . ((len f1) + (p .. f2)) = p by A2, FINSEQ_1:def_7; A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_(len_f1)_+_(p_.._f2)_holds_ not_(f1_^_f2)_._i_=_(f1_^_f2)_._((len_f1)_+_(p_.._f2)) let i be Nat; ::_thesis: ( 1 <= i & i < (len f1) + (p .. f2) implies not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2)) ) assume that A5: 1 <= i and A6: i < (len f1) + (p .. f2) ; ::_thesis: not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2)) percases ( i <= len f1 or i > len f1 ) ; suppose i <= len f1 ; ::_thesis: not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2)) then A7: i in dom f1 by A5, FINSEQ_3:25; assume (f1 ^ f2) . i = (f1 ^ f2) . ((len f1) + (p .. f2)) ; ::_thesis: contradiction then f1 . i = p by A3, A7, FINSEQ_1:def_7; then p in rng f1 by A7, FUNCT_1:def_3; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; supposeA8: i > len f1 ; ::_thesis: (f1 ^ f2) . b1 <> (f1 ^ f2) . ((len f1) + (p .. f2)) then reconsider j = i - (len f1) as Element of NAT by INT_1:5; j > 0 by A8, XREAL_1:50; then A9: 1 <= j by NAT_1:14; A10: i = j + (len f1) ; then A11: j < p .. f2 by A6, XREAL_1:6; A12: (f1 ^ f2) . ((len f1) + (p .. f2)) = f2 . (p .. f2) by A2, FINSEQ_1:def_7; A13: p .. f2 <= len f2 by A1, FINSEQ_4:21; j <= p .. f2 by A6, A10, XREAL_1:6; then j <= len f2 by A13, XXREAL_0:2; then A14: j in dom f2 by A9, FINSEQ_3:25; then (f1 ^ f2) . i = f2 . j by A10, FINSEQ_1:def_7; hence (f1 ^ f2) . i <> (f1 ^ f2) . ((len f1) + (p .. f2)) by A1, A11, A14, A12, FINSEQ_4:19, FINSEQ_4:24; ::_thesis: verum end; end; end; (len f1) + (p .. f2) in dom (f1 ^ f2) by A2, FINSEQ_1:28; hence p .. (f1 ^ f2) = (len f1) + (p .. f2) by A3, A4, Th2; ::_thesis: verum end; theorem Th8: :: FINSEQ_6:8 for f1, f2 being FinSequence for p being set st p in rng f1 holds (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 proof let f1, f2 be FinSequence; ::_thesis: for p being set st p in rng f1 holds (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 let p be set ; ::_thesis: ( p in rng f1 implies (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 ) assume A1: p in rng f1 ; ::_thesis: (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 then A2: p .. f1 = p .. (f1 ^ f2) by Th6; A3: len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def_6; A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f1_|--_p)_^_f2)_holds_ ((f1_|--_p)_^_f2)_._k_=_(f1_^_f2)_._(k_+_(p_.._(f1_^_f2))) let k be Nat; ::_thesis: ( k in dom ((f1 |-- p) ^ f2) implies ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2))) ) assume A5: k in dom ((f1 |-- p) ^ f2) ; ::_thesis: ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2))) percases ( k in dom (f1 |-- p) or ex n being Nat st ( n in dom f2 & k = (len (f1 |-- p)) + n ) ) by A5, FINSEQ_1:25; supposeA6: k in dom (f1 |-- p) ; ::_thesis: ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2))) len (f1 |-- p) = (len f1) - (p .. f1) by A1, FINSEQ_4:def_6; then A7: (len (f1 |-- p)) + (p .. f1) = len f1 ; k <= len (f1 |-- p) by A6, FINSEQ_3:25; then A8: k + (p .. f1) <= len f1 by A7, XREAL_1:6; A9: k <= k + (p .. f1) by NAT_1:11; 1 <= k by A6, FINSEQ_3:25; then 1 <= k + (p .. f1) by A9, XXREAL_0:2; then A10: k + (p .. f1) in dom f1 by A8, FINSEQ_3:25; thus ((f1 |-- p) ^ f2) . k = (f1 |-- p) . k by A6, FINSEQ_1:def_7 .= f1 . (k + (p .. f1)) by A1, A6, FINSEQ_4:def_6 .= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A2, A10, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom f2 & k = (len (f1 |-- p)) + n ) ; ::_thesis: ((f1 |-- p) ^ f2) . b1 = (f1 ^ f2) . (b1 + (p .. (f1 ^ f2))) then consider n being Nat such that A11: n in dom f2 and A12: k = (len (f1 |-- p)) + n ; thus ((f1 |-- p) ^ f2) . k = f2 . n by A11, A12, FINSEQ_1:def_7 .= (f1 ^ f2) . ((len f1) + n) by A11, FINSEQ_1:def_7 .= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A2, A3, A12 ; ::_thesis: verum end; end; end; rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then A13: p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; len ((f1 |-- p) ^ f2) = ((len f1) - (p .. f1)) + (len f2) by A3, FINSEQ_1:22 .= ((len f1) + (len f2)) - (p .. f1) .= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A2, FINSEQ_1:22 ; hence (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A13, A4, FINSEQ_4:def_6; ::_thesis: verum end; theorem Th9: :: FINSEQ_6:9 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) |-- p = f2 |-- p proof let f2, f1 be FinSequence; ::_thesis: for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) |-- p = f2 |-- p let p be set ; ::_thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) |-- p = f2 |-- p ) assume A1: p in (rng f2) \ (rng f1) ; ::_thesis: (f1 ^ f2) |-- p = f2 |-- p then A2: (len f1) + (p .. f2) = p .. (f1 ^ f2) by Th7; A3: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(f2_|--_p)_holds_ (f2_|--_p)_._k_=_(f1_^_f2)_._(k_+_(p_.._(f1_^_f2))) let k be Nat; ::_thesis: ( k in dom (f2 |-- p) implies (f2 |-- p) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2))) ) A4: k <= k + (p .. f2) by NAT_1:11; len (f2 |-- p) = (len f2) - (p .. f2) by A1, FINSEQ_4:def_6; then A5: (len (f2 |-- p)) + (p .. f2) = len f2 ; assume A6: k in dom (f2 |-- p) ; ::_thesis: (f2 |-- p) . k = (f1 ^ f2) . (k + (p .. (f1 ^ f2))) then k <= len (f2 |-- p) by FINSEQ_3:25; then A7: k + (p .. f2) <= len f2 by A5, XREAL_1:6; 1 <= k by A6, FINSEQ_3:25; then 1 <= k + (p .. f2) by A4, XXREAL_0:2; then A8: k + (p .. f2) in dom f2 by A7, FINSEQ_3:25; thus (f2 |-- p) . k = f2 . (k + (p .. f2)) by A1, A6, FINSEQ_4:def_6 .= (f1 ^ f2) . ((len f1) + (k + (p .. f2))) by A8, FINSEQ_1:def_7 .= (f1 ^ f2) . (k + (p .. (f1 ^ f2))) by A2 ; ::_thesis: verum end; rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then A9: p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; len (f2 |-- p) = (len f2) - (p .. f2) by A1, FINSEQ_4:def_6 .= ((len f1) + (len f2)) - ((len f1) + (p .. f2)) .= (len (f1 ^ f2)) - (p .. (f1 ^ f2)) by A2, FINSEQ_1:22 ; hence (f1 ^ f2) |-- p = f2 |-- p by A9, A3, FINSEQ_4:def_6; ::_thesis: verum end; theorem Th10: :: FINSEQ_6:10 for f1, f2 being FinSequence holds f1 c= f1 ^ f2 proof let f1, f2 be FinSequence; ::_thesis: f1 c= f1 ^ f2 A1: for x being set st x in dom f1 holds f1 . x = (f1 ^ f2) . x by FINSEQ_1:def_7; dom f1 c= dom (f1 ^ f2) by FINSEQ_1:26; hence f1 c= f1 ^ f2 by A1, GRFUNC_1:2; ::_thesis: verum end; theorem :: FINSEQ_6:11 for f1, f2 being FinSequence for A being set st A c= dom f1 holds (f1 ^ f2) | A = f1 | A by Th10, GRFUNC_1:27; theorem Th12: :: FINSEQ_6:12 for f1, f2 being FinSequence for p being set st p in rng f1 holds (f1 ^ f2) -| p = f1 -| p proof let f1, f2 be FinSequence; ::_thesis: for p being set st p in rng f1 holds (f1 ^ f2) -| p = f1 -| p let p be set ; ::_thesis: ( p in rng f1 implies (f1 ^ f2) -| p = f1 -| p ) assume A1: p in rng f1 ; ::_thesis: (f1 ^ f2) -| p = f1 -| p then consider n being Nat such that A2: n = (p .. f1) - 1 and A3: f1 | (Seg n) = f1 -| p by FINSEQ_4:def_5; A4: p .. f1 <= len f1 by A1, FINSEQ_4:21; n + 1 = p .. f1 by A2; then n <= p .. f1 by NAT_1:11; then n <= len f1 by A4, XXREAL_0:2; then Seg n c= Seg (len f1) by FINSEQ_1:5; then Seg n c= dom f1 by FINSEQ_1:def_3; then A5: (f1 ^ f2) | (Seg n) = f1 | (Seg n) by Th10, GRFUNC_1:27; rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then A6: p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; n = (p .. (f1 ^ f2)) - 1 by A1, A2, Th6; hence (f1 ^ f2) -| p = f1 -| p by A3, A6, A5, FINSEQ_4:def_5; ::_thesis: verum end; registration let f1 be FinSequence; let i be Nat; clusterf1 | (Seg i) -> FinSequence-like ; coherence f1 | (Seg i) is FinSequence-like by FINSEQ_1:15; end; theorem Th13: :: FINSEQ_6:13 for f1, f2, f3 being FinSequence st f1 c= f2 holds f3 ^ f1 c= f3 ^ f2 proof let f1, f2, f3 be FinSequence; ::_thesis: ( f1 c= f2 implies f3 ^ f1 c= f3 ^ f2 ) assume A1: f1 c= f2 ; ::_thesis: f3 ^ f1 c= f3 ^ f2 A2: dom (f3 ^ f1) c= dom (f3 ^ f2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f3 ^ f1) or x in dom (f3 ^ f2) ) assume A3: x in dom (f3 ^ f1) ; ::_thesis: x in dom (f3 ^ f2) then reconsider i = x as Element of NAT ; percases ( i in dom f3 or ex n being Nat st ( n in dom f1 & i = (len f3) + n ) ) by A3, FINSEQ_1:25; supposeA4: i in dom f3 ; ::_thesis: x in dom (f3 ^ f2) dom f3 c= dom (f3 ^ f2) by FINSEQ_1:26; hence x in dom (f3 ^ f2) by A4; ::_thesis: verum end; supposeA5: ex n being Nat st ( n in dom f1 & i = (len f3) + n ) ; ::_thesis: x in dom (f3 ^ f2) dom f1 c= dom f2 by A1, RELAT_1:11; hence x in dom (f3 ^ f2) by A5, FINSEQ_1:28; ::_thesis: verum end; end; end; for x being set st x in dom (f3 ^ f1) holds (f3 ^ f1) . x = (f3 ^ f2) . x proof let x be set ; ::_thesis: ( x in dom (f3 ^ f1) implies (f3 ^ f1) . x = (f3 ^ f2) . x ) assume A6: x in dom (f3 ^ f1) ; ::_thesis: (f3 ^ f1) . x = (f3 ^ f2) . x then reconsider i = x as Element of NAT ; percases ( i in dom f3 or ex n being Nat st ( n in dom f1 & i = (len f3) + n ) ) by A6, FINSEQ_1:25; supposeA7: i in dom f3 ; ::_thesis: (f3 ^ f1) . x = (f3 ^ f2) . x hence (f3 ^ f1) . x = f3 . i by FINSEQ_1:def_7 .= (f3 ^ f2) . x by A7, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA8: ex n being Nat st ( n in dom f1 & i = (len f3) + n ) ; ::_thesis: (f3 ^ f1) . x = (f3 ^ f2) . x A9: dom f1 c= dom f2 by A1, RELAT_1:11; consider k being Nat such that A10: k in dom f1 and A11: i = (len f3) + k by A8; thus (f3 ^ f1) . x = f1 . k by A10, A11, FINSEQ_1:def_7 .= f2 . k by A1, A10, GRFUNC_1:2 .= (f3 ^ f2) . x by A10, A11, A9, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence f3 ^ f1 c= f3 ^ f2 by A2, GRFUNC_1:2; ::_thesis: verum end; theorem Th14: :: FINSEQ_6:14 for f1, f2 being FinSequence for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) proof let f1, f2 be FinSequence; ::_thesis: for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) let i be Nat; ::_thesis: (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) A1: dom (f1 ^ (f2 | (Seg i))) c= Seg ((len f1) + i) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f1 ^ (f2 | (Seg i))) or x in Seg ((len f1) + i) ) assume A2: x in dom (f1 ^ (f2 | (Seg i))) ; ::_thesis: x in Seg ((len f1) + i) then reconsider j = x as Element of NAT ; percases ( j in dom f1 or ex n being Nat st ( n in dom (f2 | (Seg i)) & j = (len f1) + n ) ) by A2, FINSEQ_1:25; supposeA3: j in dom f1 ; ::_thesis: x in Seg ((len f1) + i) len f1 <= (len f1) + i by NAT_1:11; then A4: Seg (len f1) c= Seg ((len f1) + i) by FINSEQ_1:5; j in Seg (len f1) by A3, FINSEQ_1:def_3; hence x in Seg ((len f1) + i) by A4; ::_thesis: verum end; suppose ex n being Nat st ( n in dom (f2 | (Seg i)) & j = (len f1) + n ) ; ::_thesis: x in Seg ((len f1) + i) then consider k being Nat such that A5: k in dom (f2 | (Seg i)) and A6: j = (len f1) + k ; A7: k <= j by A6, NAT_1:11; dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61; then k in Seg i by A5, XBOOLE_0:def_4; then k <= i by FINSEQ_1:1; then A8: j <= (len f1) + i by A6, XREAL_1:6; 1 <= k by A5, FINSEQ_3:25; then 1 <= j by A7, XXREAL_0:2; hence x in Seg ((len f1) + i) by A8, FINSEQ_1:1; ::_thesis: verum end; end; end; A9: (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) c= dom (f1 ^ (f2 | (Seg i))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) or x in dom (f1 ^ (f2 | (Seg i))) ) assume A10: x in (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) ; ::_thesis: x in dom (f1 ^ (f2 | (Seg i))) then A11: x in dom (f1 ^ f2) by XBOOLE_0:def_4; reconsider j = x as Element of NAT by A10; percases ( j in dom f1 or ex n being Nat st ( n in dom f2 & j = (len f1) + n ) ) by A11, FINSEQ_1:25; supposeA12: j in dom f1 ; ::_thesis: x in dom (f1 ^ (f2 | (Seg i))) dom f1 c= dom (f1 ^ (f2 | (Seg i))) by FINSEQ_1:26; hence x in dom (f1 ^ (f2 | (Seg i))) by A12; ::_thesis: verum end; suppose ex n being Nat st ( n in dom f2 & j = (len f1) + n ) ; ::_thesis: x in dom (f1 ^ (f2 | (Seg i))) then consider k being Nat such that A13: k in dom f2 and A14: j = (len f1) + k ; A15: 1 <= k by A13, FINSEQ_3:25; A16: dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61; j in Seg ((len f1) + i) by A10, XBOOLE_0:def_4; then j <= (len f1) + i by FINSEQ_1:1; then k <= i by A14, XREAL_1:6; then k in Seg i by A15, FINSEQ_1:1; then k in dom (f2 | (Seg i)) by A13, A16, XBOOLE_0:def_4; hence x in dom (f1 ^ (f2 | (Seg i))) by A14, FINSEQ_1:28; ::_thesis: verum end; end; end; A17: dom ((f1 ^ f2) | (Seg ((len f1) + i))) = (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by RELAT_1:61; A18: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f1_^_f2)_|_(Seg_((len_f1)_+_i)))_holds_ ((f1_^_f2)_|_(Seg_((len_f1)_+_i)))_._k_=_(f1_^_(f2_|_(Seg_i)))_._k let k be Nat; ::_thesis: ( k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) implies ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 ) assume A19: k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) ; ::_thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 then A20: 1 <= k by FINSEQ_3:25; percases ( k <= len f1 or k > len f1 ) ; suppose k <= len f1 ; ::_thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 then A21: k in dom f1 by A20, FINSEQ_3:25; thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A19, FUNCT_1:47 .= f1 . k by A21, FINSEQ_1:def_7 .= (f1 ^ (f2 | (Seg i))) . k by A21, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA22: k > len f1 ; ::_thesis: ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 then reconsider j = k - (len f1) as Element of NAT by INT_1:5; j > 0 by A22, XREAL_1:50; then A23: 1 <= j by NAT_1:14; A24: k = (len f1) + j ; A25: not k in dom f1 by A22, FINSEQ_3:25; k in dom (f1 ^ f2) by A17, A19, XBOOLE_0:def_4; then A26: ex n being Nat st ( n in dom f2 & k = (len f1) + n ) by A25, FINSEQ_1:25; k in Seg ((len f1) + i) by A17, A19, XBOOLE_0:def_4; then k <= (len f1) + i by FINSEQ_1:1; then j <= i by A24, XREAL_1:6; then A27: j in Seg i by A23, FINSEQ_1:1; dom (f2 | (Seg i)) = (dom f2) /\ (Seg i) by RELAT_1:61; then A28: j in dom (f2 | (Seg i)) by A27, A26, XBOOLE_0:def_4; thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ f2) . k by A19, FUNCT_1:47 .= f2 . j by A26, FINSEQ_1:def_7 .= (f2 | (Seg i)) . j by A28, FUNCT_1:47 .= (f1 ^ (f2 | (Seg i))) . k by A24, A28, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; f1 ^ (f2 | (Seg i)) c= f1 ^ f2 by Th13, RELAT_1:59; then dom (f1 ^ (f2 | (Seg i))) c= dom (f1 ^ f2) by RELAT_1:11; then dom (f1 ^ (f2 | (Seg i))) c= (dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) by A1, XBOOLE_1:19; then dom ((f1 ^ f2) | (Seg ((len f1) + i))) = dom (f1 ^ (f2 | (Seg i))) by A17, A9, XBOOLE_0:def_10; hence (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) by A18, FINSEQ_1:13; ::_thesis: verum end; theorem Th15: :: FINSEQ_6:15 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -| p = f1 ^ (f2 -| p) proof let f2, f1 be FinSequence; ::_thesis: for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -| p = f1 ^ (f2 -| p) let p be set ; ::_thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) -| p = f1 ^ (f2 -| p) ) assume A1: p in (rng f2) \ (rng f1) ; ::_thesis: (f1 ^ f2) -| p = f1 ^ (f2 -| p) then consider n being Nat such that A2: n = (p .. f2) - 1 and A3: f2 | (Seg n) = f2 -| p by FINSEQ_4:def_5; p .. (f1 ^ f2) = (len f1) + (p .. f2) by A1, Th7; then A4: (len f1) + n = (p .. (f1 ^ f2)) - 1 by A2; rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then A5: p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; (f1 ^ f2) | (Seg ((len f1) + n)) = f1 ^ (f2 -| p) by A3, Th14; hence (f1 ^ f2) -| p = f1 ^ (f2 -| p) by A5, A4, FINSEQ_4:def_5; ::_thesis: verum end; theorem Th16: :: FINSEQ_6:16 for f1, f2 being FinSequence for p being set st f1 ^ f2 just_once_values p holds p in (rng f1) \+\ (rng f2) proof let f1, f2 be FinSequence; ::_thesis: for p being set st f1 ^ f2 just_once_values p holds p in (rng f1) \+\ (rng f2) let p be set ; ::_thesis: ( f1 ^ f2 just_once_values p implies p in (rng f1) \+\ (rng f2) ) A1: rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; assume A2: f1 ^ f2 just_once_values p ; ::_thesis: p in (rng f1) \+\ (rng f2) A3: now__::_thesis:_not_p_in_(rng_f1)_/\_(rng_f2) assume A4: p in (rng f1) /\ (rng f2) ; ::_thesis: contradiction then p in rng f1 by XBOOLE_0:def_4; then (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by Th8; then A5: not p in rng ((f1 |-- p) ^ f2) by A2, FINSEQ_4:45; rng ((f1 |-- p) ^ f2) = (rng (f1 |-- p)) \/ (rng f2) by FINSEQ_1:31; then not p in rng f2 by A5, XBOOLE_0:def_3; hence contradiction by A4, XBOOLE_0:def_4; ::_thesis: verum end; p in rng (f1 ^ f2) by A2, FINSEQ_4:5; then p in ((rng f1) \/ (rng f2)) \ ((rng f1) /\ (rng f2)) by A1, A3, XBOOLE_0:def_5; hence p in (rng f1) \+\ (rng f2) by XBOOLE_1:101; ::_thesis: verum end; theorem :: FINSEQ_6:17 for f1, f2 being FinSequence for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds f1 just_once_values p proof let f1, f2 be FinSequence; ::_thesis: for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds f1 just_once_values p let p be set ; ::_thesis: ( f1 ^ f2 just_once_values p & p in rng f1 implies f1 just_once_values p ) assume that A1: f1 ^ f2 just_once_values p and A2: p in rng f1 ; ::_thesis: f1 just_once_values p (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A2, Th8; then A3: rng ((f1 ^ f2) |-- p) = (rng (f1 |-- p)) \/ (rng f2) by FINSEQ_1:31; not p in rng ((f1 ^ f2) |-- p) by A1, FINSEQ_4:45; then not p in rng (f1 |-- p) by A3, XBOOLE_0:def_3; hence f1 just_once_values p by A2, FINSEQ_4:45; ::_thesis: verum end; theorem Th18: :: FINSEQ_6:18 for p being set holds p .. <*p*> = 1 proof let p be set ; ::_thesis: p .. <*p*> = 1 A1: for i being Nat st 1 <= i & i < 1 holds <*p*> . i <> <*p*> . 1 ; dom <*p*> = Seg 1 by FINSEQ_1:38; then A2: 1 in dom <*p*> by FINSEQ_1:2, TARSKI:def_1; <*p*> . 1 = p by FINSEQ_1:40; hence p .. <*p*> = 1 by A2, A1, Th2; ::_thesis: verum end; theorem Th19: :: FINSEQ_6:19 for p1, p2 being set holds p1 .. <*p1,p2*> = 1 proof let p1, p2 be set ; ::_thesis: p1 .. <*p1,p2*> = 1 A1: for i being Nat st 1 <= i & i < 1 holds <*p1,p2*> . i <> <*p1,p2*> . 1 ; len <*p1,p2*> = 2 by FINSEQ_1:44; then A2: 1 in dom <*p1,p2*> by FINSEQ_3:25; <*p1,p2*> . 1 = p1 by FINSEQ_1:44; hence p1 .. <*p1,p2*> = 1 by A2, A1, Th2; ::_thesis: verum end; theorem Th20: :: FINSEQ_6:20 for p1, p2 being set st p1 <> p2 holds p2 .. <*p1,p2*> = 2 proof let p1, p2 be set ; ::_thesis: ( p1 <> p2 implies p2 .. <*p1,p2*> = 2 ) A1: <*p1,p2*> . 2 = p2 by FINSEQ_1:44; A2: <*p1,p2*> . 1 = p1 by FINSEQ_1:44; assume A3: p1 <> p2 ; ::_thesis: p2 .. <*p1,p2*> = 2 A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_1_+_1_holds_ <*p1,p2*>_._i_<>_<*p1,p2*>_._2 let i be Nat; ::_thesis: ( 1 <= i & i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 ) assume A5: 1 <= i ; ::_thesis: ( i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 ) assume i < 1 + 1 ; ::_thesis: <*p1,p2*> . i <> <*p1,p2*> . 2 then i <= 1 by NAT_1:13; hence <*p1,p2*> . i <> <*p1,p2*> . 2 by A3, A1, A2, A5, XXREAL_0:1; ::_thesis: verum end; 2 <= len <*p1,p2*> by FINSEQ_1:44; then 2 in dom <*p1,p2*> by FINSEQ_3:25; hence p2 .. <*p1,p2*> = 2 by A1, A4, Th2; ::_thesis: verum end; theorem Th21: :: FINSEQ_6:21 for p1, p2, p3 being set holds p1 .. <*p1,p2,p3*> = 1 proof let p1, p2, p3 be set ; ::_thesis: p1 .. <*p1,p2,p3*> = 1 A1: for i being Nat st 1 <= i & i < 1 holds <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 1 ; len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then A2: 1 in dom <*p1,p2,p3*> by FINSEQ_3:25; <*p1,p2,p3*> . 1 = p1 by FINSEQ_1:45; hence p1 .. <*p1,p2,p3*> = 1 by A2, A1, Th2; ::_thesis: verum end; theorem Th22: :: FINSEQ_6:22 for p1, p2, p3 being set st p1 <> p2 holds p2 .. <*p1,p2,p3*> = 2 proof let p1, p2, p3 be set ; ::_thesis: ( p1 <> p2 implies p2 .. <*p1,p2,p3*> = 2 ) A1: <*p1,p2,p3*> . 2 = p2 by FINSEQ_1:45; A2: <*p1,p2,p3*> . 1 = p1 by FINSEQ_1:45; assume A3: p1 <> p2 ; ::_thesis: p2 .. <*p1,p2,p3*> = 2 A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_1_+_1_holds_ <*p1,p2,p3*>_._i_<>_<*p1,p2,p3*>_._2 let i be Nat; ::_thesis: ( 1 <= i & i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 ) assume A5: 1 <= i ; ::_thesis: ( i < 1 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 ) assume i < 1 + 1 ; ::_thesis: <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 then i <= 1 by NAT_1:13; hence <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 2 by A3, A1, A2, A5, XXREAL_0:1; ::_thesis: verum end; len <*p1,p2,p3*> = 3 by FINSEQ_1:45; then 2 in dom <*p1,p2,p3*> by FINSEQ_3:25; hence p2 .. <*p1,p2,p3*> = 2 by A1, A4, Th2; ::_thesis: verum end; theorem Th23: :: FINSEQ_6:23 for p1, p3, p2 being set st p1 <> p3 & p2 <> p3 holds p3 .. <*p1,p2,p3*> = 3 proof let p1, p3, p2 be set ; ::_thesis: ( p1 <> p3 & p2 <> p3 implies p3 .. <*p1,p2,p3*> = 3 ) assume that A1: p1 <> p3 and A2: p2 <> p3 ; ::_thesis: p3 .. <*p1,p2,p3*> = 3 A3: <*p1,p2,p3*> . 3 = p3 by FINSEQ_1:45; A4: <*p1,p2,p3*> . 1 = p1 by FINSEQ_1:45; A5: <*p1,p2,p3*> . 2 = p2 by FINSEQ_1:45; A6: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_2_+_1_holds_ <*p1,p2,p3*>_._i_<>_<*p1,p2,p3*>_._3 let i be Nat; ::_thesis: ( 1 <= i & i < 2 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 3 ) assume 1 <= i ; ::_thesis: ( i < 2 + 1 implies <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 3 ) then A7: i <> 0 ; assume i < 2 + 1 ; ::_thesis: <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 3 then i <= 2 by NAT_1:13; hence <*p1,p2,p3*> . i <> <*p1,p2,p3*> . 3 by A1, A2, A3, A5, A4, A7, NAT_1:26; ::_thesis: verum end; 3 <= len <*p1,p2,p3*> by FINSEQ_1:45; then 3 in dom <*p1,p2,p3*> by FINSEQ_3:25; hence p3 .. <*p1,p2,p3*> = 3 by A3, A6, Th2; ::_thesis: verum end; theorem Th24: :: FINSEQ_6:24 for p being set for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*> proof let p be set ; ::_thesis: for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*> let f be FinSequence; ::_thesis: Rev (<*p*> ^ f) = (Rev f) ^ <*p*> thus Rev (<*p*> ^ f) = (Rev f) ^ (Rev <*p*>) by FINSEQ_5:64 .= (Rev f) ^ <*p*> by FINSEQ_5:60 ; ::_thesis: verum end; theorem :: FINSEQ_6:25 for f being FinSequence holds Rev (Rev f) = f ; theorem Th26: :: FINSEQ_6:26 for x, y being set st x <> y holds <*x,y*> -| y = <*x*> proof let x, y be set ; ::_thesis: ( x <> y implies <*x,y*> -| y = <*x*> ) assume x <> y ; ::_thesis: <*x,y*> -| y = <*x*> then y .. <*x,y*> = 1 + 1 by Th20; then A1: 1 = (y .. <*x,y*>) - 1 ; rng <*x,y*> = {x,y} by Lm1; then y in rng <*x,y*> by TARSKI:def_2; hence <*x,y*> -| y = <*x,y*> | (Seg 1) by A1, FINSEQ_4:33 .= <*x*> by Th3 ; ::_thesis: verum end; theorem Th27: :: FINSEQ_6:27 for x, y, z being set st x <> y holds <*x,y,z*> -| y = <*x*> proof let x, y, z be set ; ::_thesis: ( x <> y implies <*x,y,z*> -| y = <*x*> ) assume x <> y ; ::_thesis: <*x,y,z*> -| y = <*x*> then y .. <*x,y,z*> = 1 + 1 by Th22; then A1: 1 = (y .. <*x,y,z*>) - 1 ; rng <*x,y,z*> = {x,y,z} by Lm2; then y in rng <*x,y,z*> by ENUMSET1:def_1; hence <*x,y,z*> -| y = <*x,y,z*> | (Seg 1) by A1, FINSEQ_4:33 .= <*x*> by Th4 ; ::_thesis: verum end; theorem Th28: :: FINSEQ_6:28 for x, z, y being set st x <> z & y <> z holds <*x,y,z*> -| z = <*x,y*> proof let x, z, y be set ; ::_thesis: ( x <> z & y <> z implies <*x,y,z*> -| z = <*x,y*> ) assume that A1: x <> z and A2: y <> z ; ::_thesis: <*x,y,z*> -| z = <*x,y*> rng <*x,y,z*> = {x,y,z} by Lm2; then A3: z in rng <*x,y,z*> by ENUMSET1:def_1; z .. <*x,y,z*> = 2 + 1 by A1, A2, Th23; then 2 = (z .. <*x,y,z*>) - 1 ; hence <*x,y,z*> -| z = <*x,y,z*> | (Seg 2) by A3, FINSEQ_4:33 .= <*x,y*> by Th5 ; ::_thesis: verum end; theorem :: FINSEQ_6:29 for x, y being set holds <*x,y*> |-- x = <*y*> proof let x, y be set ; ::_thesis: <*x,y*> |-- x = <*y*> A1: x .. <*x,y*> = 1 by Th19; then (len <*y*>) + (x .. <*x,y*>) = 1 + 1 by FINSEQ_1:40 .= len <*x,y*> by FINSEQ_1:44 ; then A2: len <*y*> = (len <*x,y*>) - (x .. <*x,y*>) ; A3: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<*y*>_holds_ <*y*>_._k_=_<*x,y*>_._(k_+_(x_.._<*x,y*>)) let k be Nat; ::_thesis: ( k in dom <*y*> implies <*y*> . k = <*x,y*> . (k + (x .. <*x,y*>)) ) assume k in dom <*y*> ; ::_thesis: <*y*> . k = <*x,y*> . (k + (x .. <*x,y*>)) then k in Seg 1 by FINSEQ_1:38; then A4: k = 1 by FINSEQ_1:2, TARSKI:def_1; hence <*y*> . k = y by FINSEQ_1:40 .= <*x,y*> . (k + (x .. <*x,y*>)) by A1, A4, FINSEQ_1:44 ; ::_thesis: verum end; x in {x,y} by TARSKI:def_2; then x in rng <*x,y*> by Lm1; hence <*x,y*> |-- x = <*y*> by A2, A3, FINSEQ_4:def_6; ::_thesis: verum end; theorem Th30: :: FINSEQ_6:30 for x, y, z being set st x <> y holds <*x,y,z*> |-- y = <*z*> proof let x, y, z be set ; ::_thesis: ( x <> y implies <*x,y,z*> |-- y = <*z*> ) assume x <> y ; ::_thesis: <*x,y,z*> |-- y = <*z*> then A1: y .. <*x,y,z*> = 2 by Th22; then (len <*z*>) + (y .. <*x,y,z*>) = 1 + 2 by FINSEQ_1:40 .= len <*x,y,z*> by FINSEQ_1:45 ; then A2: len <*z*> = (len <*x,y,z*>) - (y .. <*x,y,z*>) ; A3: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<*z*>_holds_ <*z*>_._k_=_<*x,y,z*>_._(k_+_(y_.._<*x,y,z*>)) let k be Nat; ::_thesis: ( k in dom <*z*> implies <*z*> . k = <*x,y,z*> . (k + (y .. <*x,y,z*>)) ) assume k in dom <*z*> ; ::_thesis: <*z*> . k = <*x,y,z*> . (k + (y .. <*x,y,z*>)) then k in Seg 1 by FINSEQ_1:38; then A4: k = 1 by FINSEQ_1:2, TARSKI:def_1; hence <*z*> . k = z by FINSEQ_1:40 .= <*x,y,z*> . (k + (y .. <*x,y,z*>)) by A1, A4, FINSEQ_1:45 ; ::_thesis: verum end; y in {x,y,z} by ENUMSET1:def_1; then y in rng <*x,y,z*> by Lm2; hence <*x,y,z*> |-- y = <*z*> by A2, A3, FINSEQ_4:def_6; ::_thesis: verum end; theorem :: FINSEQ_6:31 for x, y, z being set holds <*x,y,z*> |-- x = <*y,z*> proof let x, y, z be set ; ::_thesis: <*x,y,z*> |-- x = <*y,z*> A1: x .. <*x,y,z*> = 1 by Th21; then (len <*y,z*>) + (x .. <*x,y,z*>) = 2 + 1 by FINSEQ_1:44 .= len <*x,y,z*> by FINSEQ_1:45 ; then A2: len <*y,z*> = (len <*x,y,z*>) - (x .. <*x,y,z*>) ; A3: len <*y,z*> = 2 by FINSEQ_1:44; A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<*y,z*>_holds_ <*y,z*>_._k_=_<*x,y,z*>_._(k_+_(x_.._<*x,y,z*>)) let k be Nat; ::_thesis: ( k in dom <*y,z*> implies <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) ) assume k in dom <*y,z*> ; ::_thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) then A5: k in Seg 2 by A3, FINSEQ_1:def_3; percases ( k = 1 or k = 2 ) by A5, FINSEQ_1:2, TARSKI:def_2; supposeA6: k = 1 ; ::_thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) hence <*y,z*> . k = y by FINSEQ_1:44 .= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A1, A6, FINSEQ_1:45 ; ::_thesis: verum end; supposeA7: k = 2 ; ::_thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) hence <*y,z*> . k = z by FINSEQ_1:44 .= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A1, A7, FINSEQ_1:45 ; ::_thesis: verum end; end; end; x in {x,y,z} by ENUMSET1:def_1; then x in rng <*x,y,z*> by Lm2; hence <*x,y,z*> |-- x = <*y,z*> by A2, A4, FINSEQ_4:def_6; ::_thesis: verum end; theorem Th32: :: FINSEQ_6:32 for z being set holds ( <*z*> |-- z = {} & <*z*> -| z = {} ) proof let z be set ; ::_thesis: ( <*z*> |-- z = {} & <*z*> -| z = {} ) z in {z} by TARSKI:def_1; then A1: z in rng <*z*> by FINSEQ_1:39; A2: z .. <*z*> = 1 by Th18; len <*z*> = 1 by FINSEQ_1:39; hence <*z*> |-- z = {} by A1, A2, FINSEQ_4:49; ::_thesis: <*z*> -| z = {} thus <*z*> -| z = {} by A1, A2, FINSEQ_4:40; ::_thesis: verum end; theorem Th33: :: FINSEQ_6:33 for x, y being set st x <> y holds <*x,y*> |-- y = {} proof let x, y be set ; ::_thesis: ( x <> y implies <*x,y*> |-- y = {} ) y in {x,y} by TARSKI:def_2; then A1: y in rng <*x,y*> by Lm1; assume x <> y ; ::_thesis: <*x,y*> |-- y = {} then A2: y .. <*x,y*> = 2 by Th20; len <*x,y*> = 2 by FINSEQ_1:44; hence <*x,y*> |-- y = {} by A1, A2, FINSEQ_4:49; ::_thesis: verum end; theorem Th34: :: FINSEQ_6:34 for x, z, y being set st x <> z & y <> z holds <*x,y,z*> |-- z = {} proof let x, z, y be set ; ::_thesis: ( x <> z & y <> z implies <*x,y,z*> |-- z = {} ) assume that A1: x <> z and A2: y <> z ; ::_thesis: <*x,y,z*> |-- z = {} A3: len <*x,y,z*> = 3 by FINSEQ_1:45; z in {x,y,z} by ENUMSET1:def_1; then A4: z in rng <*x,y,z*> by Lm2; z .. <*x,y,z*> = 3 by A1, A2, Th23; hence <*x,y,z*> |-- z = {} by A4, A3, FINSEQ_4:49; ::_thesis: verum end; theorem Th35: :: FINSEQ_6:35 for x, y being set for f being FinSequence st x in rng f & y in rng (f -| x) holds (f -| x) -| y = f -| y proof let x, y be set ; ::_thesis: for f being FinSequence st x in rng f & y in rng (f -| x) holds (f -| x) -| y = f -| y let f be FinSequence; ::_thesis: ( x in rng f & y in rng (f -| x) implies (f -| x) -| y = f -| y ) assume that A1: x in rng f and A2: y in rng (f -| x) ; ::_thesis: (f -| x) -| y = f -| y thus f -| y = (((f -| x) ^ <*x*>) ^ (f |-- x)) -| y by A1, FINSEQ_4:51 .= ((f -| x) ^ (<*x*> ^ (f |-- x))) -| y by FINSEQ_1:32 .= (f -| x) -| y by A2, Th12 ; ::_thesis: verum end; theorem Th36: :: FINSEQ_6:36 for x being set for f1, f2 being FinSequence st not x in rng f1 holds x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 proof let x be set ; ::_thesis: for f1, f2 being FinSequence st not x in rng f1 holds x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 let f1, f2 be FinSequence; ::_thesis: ( not x in rng f1 implies x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 ) x in {x} by TARSKI:def_1; then A1: x in rng <*x*> by FINSEQ_1:38; assume not x in rng f1 ; ::_thesis: x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 then x in (rng <*x*>) \ (rng f1) by A1, XBOOLE_0:def_5; then A2: (f1 ^ <*x*>) |-- x = <*x*> |-- x by Th9 .= {} by Th32 ; rng (f1 ^ <*x*>) = (rng f1) \/ (rng <*x*>) by FINSEQ_1:31; then A3: x in rng (f1 ^ <*x*>) by A1, XBOOLE_0:def_3; then (len (f1 ^ <*x*>)) - (x .. (f1 ^ <*x*>)) = len ((f1 ^ <*x*>) |-- x) by FINSEQ_4:def_6 .= 0 by A2 ; hence x .. ((f1 ^ <*x*>) ^ f2) = len (f1 ^ <*x*>) by A3, Th6 .= (len f1) + (len <*x*>) by FINSEQ_1:22 .= (len f1) + 1 by FINSEQ_1:39 ; ::_thesis: verum end; theorem Th37: :: FINSEQ_6:37 for x being set for f being FinSequence st f just_once_values x holds (x .. f) + (x .. (Rev f)) = (len f) + 1 proof let x be set ; ::_thesis: for f being FinSequence st f just_once_values x holds (x .. f) + (x .. (Rev f)) = (len f) + 1 let f be FinSequence; ::_thesis: ( f just_once_values x implies (x .. f) + (x .. (Rev f)) = (len f) + 1 ) assume A1: f just_once_values x ; ::_thesis: (x .. f) + (x .. (Rev f)) = (len f) + 1 then A2: x in rng f by FINSEQ_4:5; then A3: f = ((f -| x) ^ <*x*>) ^ (f |-- x) by FINSEQ_4:51; then A4: len f = (len ((f -| x) ^ <*x*>)) + (len (f |-- x)) by FINSEQ_1:22 .= ((len (f -| x)) + (len <*x*>)) + (len (f |-- x)) by FINSEQ_1:22 .= ((len (f -| x)) + 1) + (len (f |-- x)) by FINSEQ_1:39 ; not x in rng (f |-- x) by A1, FINSEQ_4:45; then A5: not x in rng (Rev (f |-- x)) by FINSEQ_5:57; Rev f = (Rev (f |-- x)) ^ (Rev ((f -| x) ^ <*x*>)) by A3, FINSEQ_5:64 .= (Rev (f |-- x)) ^ (<*x*> ^ (Rev (f -| x))) by FINSEQ_5:63 .= ((Rev (f |-- x)) ^ <*x*>) ^ (Rev (f -| x)) by FINSEQ_1:32 ; then A6: x .. (Rev f) = (len (Rev (f |-- x))) + 1 by A5, Th36; (len (f -| x)) + 1 = ((x .. f) - 1) + 1 by A2, FINSEQ_4:34 .= x .. f ; hence (x .. f) + (x .. (Rev f)) = (((len (f -| x)) + 1) + (len (Rev (f |-- x)))) + 1 by A6 .= (len f) + 1 by A4, FINSEQ_5:def_3 ; ::_thesis: verum end; theorem Th38: :: FINSEQ_6:38 for x being set for f being FinSequence st f just_once_values x holds Rev (f -| x) = (Rev f) |-- x proof let x be set ; ::_thesis: for f being FinSequence st f just_once_values x holds Rev (f -| x) = (Rev f) |-- x let f be FinSequence; ::_thesis: ( f just_once_values x implies Rev (f -| x) = (Rev f) |-- x ) A1: len (Rev (f -| x)) = len (f -| x) by FINSEQ_5:def_3; assume A2: f just_once_values x ; ::_thesis: Rev (f -| x) = (Rev f) |-- x then A3: x in rng f by FINSEQ_4:5; then A4: x in rng (Rev f) by FINSEQ_5:57; A5: (x .. f) + (x .. (Rev f)) = (len f) + 1 by A2, Th37; A6: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Rev_(f_-|_x))_holds_ (Rev_(f_-|_x))_._k_=_(Rev_f)_._(k_+_(x_.._(Rev_f))) let k be Nat; ::_thesis: ( k in dom (Rev (f -| x)) implies (Rev (f -| x)) . k = (Rev f) . (k + (x .. (Rev f))) ) consider m being Nat such that m = (x .. f) - 1 and A7: f -| x = f | (Seg m) by A3, FINSEQ_4:def_5; assume A8: k in dom (Rev (f -| x)) ; ::_thesis: (Rev (f -| x)) . k = (Rev f) . (k + (x .. (Rev f))) then A9: 1 <= k by FINSEQ_3:25; then A10: (x .. f) - k <= (x .. f) - 1 by XREAL_1:13; A11: len (f -| x) = (x .. f) - 1 by A3, FINSEQ_4:34; k in dom (f -| x) by A8, FINSEQ_5:57; then k <= (x .. f) - 1 by A11, FINSEQ_3:25; then A12: k + 1 <= x .. f by XREAL_1:19; then k < x .. f by NAT_1:13; then k + (x .. (Rev f)) < (len f) + 1 by A5, XREAL_1:6; then k + (x .. (Rev f)) <= len f by NAT_1:13; then A13: k + (x .. (Rev f)) <= len (Rev f) by FINSEQ_5:def_3; A14: 1 <= (x .. f) - k by A12, XREAL_1:19; then 0 <= (x .. f) - k ; then (x .. f) - k is Element of NAT by INT_1:5, XREAL_1:49; then A15: (((x .. f) - 1) - k) + 1 in dom (f | (Seg m)) by A7, A11, A14, A10, FINSEQ_3:25; k <= k + (x .. (Rev f)) by NAT_1:11; then 1 <= k + (x .. (Rev f)) by A9, XXREAL_0:2; then A16: k + (x .. (Rev f)) in dom (Rev f) by A13, FINSEQ_3:25; thus (Rev (f -| x)) . k = (f -| x) . ((((x .. f) - 1) - k) + 1) by A8, A11, FINSEQ_5:def_3 .= f . (((len f) - (k + (x .. (Rev f)))) + 1) by A5, A7, A15, FUNCT_1:47 .= (Rev f) . (k + (x .. (Rev f))) by A16, FINSEQ_5:def_3 ; ::_thesis: verum end; len (f -| x) = (x .. f) - 1 by A3, FINSEQ_4:34 .= (len f) - (x .. (Rev f)) by A5 .= (len (Rev f)) - (x .. (Rev f)) by FINSEQ_5:def_3 ; hence Rev (f -| x) = (Rev f) |-- x by A4, A1, A6, FINSEQ_4:def_6; ::_thesis: verum end; theorem :: FINSEQ_6:39 for x being set for f being FinSequence st f just_once_values x holds Rev f just_once_values x proof let x be set ; ::_thesis: for f being FinSequence st f just_once_values x holds Rev f just_once_values x let f be FinSequence; ::_thesis: ( f just_once_values x implies Rev f just_once_values x ) assume A1: f just_once_values x ; ::_thesis: Rev f just_once_values x then A2: x in rng f by FINSEQ_4:5; then not x in rng (f -| x) by FINSEQ_4:37; then not x in rng (Rev (f -| x)) by FINSEQ_5:57; then A3: not x in rng ((Rev f) |-- x) by A1, Th38; x in rng (Rev f) by A2, FINSEQ_5:57; hence Rev f just_once_values x by A3, FINSEQ_4:45; ::_thesis: verum end; begin theorem Th40: :: FINSEQ_6:40 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f -: p = (f -| p) ^ <*p*> proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds f -: p = (f -| p) ^ <*p*> let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds f -: p = (f -| p) ^ <*p*> let f be FinSequence of D; ::_thesis: ( p in rng f implies f -: p = (f -| p) ^ <*p*> ) assume p in rng f ; ::_thesis: f -: p = (f -| p) ^ <*p*> hence (f -| p) ^ <*p*> = f | (p .. f) by FINSEQ_5:24 .= f -: p by FINSEQ_5:def_1 ; ::_thesis: verum end; theorem Th41: :: FINSEQ_6:41 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f :- p = <*p*> ^ (f |-- p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds f :- p = <*p*> ^ (f |-- p) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds f :- p = <*p*> ^ (f |-- p) let f be FinSequence of D; ::_thesis: ( p in rng f implies f :- p = <*p*> ^ (f |-- p) ) assume p in rng f ; ::_thesis: f :- p = <*p*> ^ (f |-- p) hence <*p*> ^ (f |-- p) = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:35 .= f :- p by FINSEQ_5:def_2 ; ::_thesis: verum end; theorem Th42: :: FINSEQ_6:42 for D being non empty set for f being FinSequence of D st f <> {} holds f /. 1 in rng f proof let D be non empty set ; ::_thesis: for f being FinSequence of D st f <> {} holds f /. 1 in rng f let f be FinSequence of D; ::_thesis: ( f <> {} implies f /. 1 in rng f ) assume f <> {} ; ::_thesis: f /. 1 in rng f then 1 in dom f by FINSEQ_5:6; hence f /. 1 in rng f by PARTFUN2:2; ::_thesis: verum end; theorem Th43: :: FINSEQ_6:43 for D being non empty set for f being FinSequence of D st f <> {} holds (f /. 1) .. f = 1 proof let D be non empty set ; ::_thesis: for f being FinSequence of D st f <> {} holds (f /. 1) .. f = 1 let f be FinSequence of D; ::_thesis: ( f <> {} implies (f /. 1) .. f = 1 ) assume f <> {} ; ::_thesis: (f /. 1) .. f = 1 then A1: 1 in dom f by FINSEQ_5:6; f /. 1 in {(f /. 1)} by TARSKI:def_1; then A2: 1 in f " {(f /. 1)} by A1, PARTFUN2:26; f " {(f /. 1)} c= dom f by RELAT_1:132; then A3: f " {(f /. 1)} c= Seg (len f) by FINSEQ_1:def_3; thus (f /. 1) .. f = (Sgm (f " {(f /. 1)})) . 1 by FINSEQ_4:def_4 .= 1 by A3, A2, Th1 ; ::_thesis: verum end; theorem Th44: :: FINSEQ_6:44 for D being non empty set for p being Element of D for f being FinSequence of D st f <> {} & f /. 1 = p holds ( f -: p = <*p*> & f :- p = f ) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f <> {} & f /. 1 = p holds ( f -: p = <*p*> & f :- p = f ) let p be Element of D; ::_thesis: for f being FinSequence of D st f <> {} & f /. 1 = p holds ( f -: p = <*p*> & f :- p = f ) let f be FinSequence of D; ::_thesis: ( f <> {} & f /. 1 = p implies ( f -: p = <*p*> & f :- p = f ) ) assume that A1: f <> {} and A2: f /. 1 = p ; ::_thesis: ( f -: p = <*p*> & f :- p = f ) A3: p in rng f by A1, A2, Th42; p .. f = 1 by A1, A2, Th43; then A4: f -| p = {} by A3, FINSEQ_4:40; hence f -: p = {} ^ <*p*> by A3, Th40 .= <*p*> by FINSEQ_1:34 ; ::_thesis: f :- p = f thus f = ({} ^ <*p*>) ^ (f |-- p) by A3, A4, FINSEQ_4:51 .= <*p*> ^ (f |-- p) by FINSEQ_1:34 .= f :- p by A3, Th41 ; ::_thesis: verum end; theorem Th45: :: FINSEQ_6:45 for D being non empty set for p1 being Element of D for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f proof let D be non empty set ; ::_thesis: for p1 being Element of D for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f let p1 be Element of D; ::_thesis: for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f let f be FinSequence of D; ::_thesis: (<*p1*> ^ f) /^ 1 = f A1: (<*p1*> ^ f) /. 1 = p1 by FINSEQ_5:15; 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1; then A2: 1 in dom <*p1*> by FINSEQ_1:38; dom <*p1*> c= dom (<*p1*> ^ f) by FINSEQ_1:26; then <*((<*p1*> ^ f) /. (0 + 1))*> ^ ((<*p1*> ^ f) /^ 1) = (<*p1*> ^ f) /^ 0 by A2, FINSEQ_5:31 .= <*p1*> ^ f by FINSEQ_5:28 ; hence (<*p1*> ^ f) /^ 1 = f by A1, FINSEQ_1:33; ::_thesis: verum end; theorem Th46: :: FINSEQ_6:46 for D being non empty set for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*> let p1, p2 be Element of D; ::_thesis: <*p1,p2*> /^ 1 = <*p2*> <*p1,p2*> = <*p1*> ^ <*p2*> by FINSEQ_1:def_9; hence <*p1,p2*> /^ 1 = <*p2*> by Th45; ::_thesis: verum end; theorem Th47: :: FINSEQ_6:47 for D being non empty set for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*> let p1, p2, p3 be Element of D; ::_thesis: <*p1,p2,p3*> /^ 1 = <*p2,p3*> <*p1,p2,p3*> = <*p1*> ^ <*p2,p3*> by FINSEQ_1:43; hence <*p1,p2,p3*> /^ 1 = <*p2,p3*> by Th45; ::_thesis: verum end; theorem Th48: :: FINSEQ_6:48 for k being Nat for D being non empty set for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ) holds (f /. k) .. f = k proof let k be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ) holds (f /. k) .. f = k let D be non empty set ; ::_thesis: for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ) holds (f /. k) .. f = k let f be FinSequence of D; ::_thesis: ( k in dom f & ( for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ) implies (f /. k) .. f = k ) assume that A1: k in dom f and A2: for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ; ::_thesis: (f /. k) .. f = k A3: f /. k in rng f by A1, PARTFUN2:2; assume A4: (f /. k) .. f <> k ; ::_thesis: contradiction (f /. k) .. f <= k by A1, FINSEQ_5:39; then (f /. k) .. f < k by A4, XXREAL_0:1; then f /. ((f /. k) .. f) <> f /. k by A2, A3, FINSEQ_4:21; hence contradiction by A3, FINSEQ_5:38; ::_thesis: verum end; theorem Th49: :: FINSEQ_6:49 for D being non empty set for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> -: p2 = <*p1,p2*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> -: p2 = <*p1,p2*> let p1, p2 be Element of D; ::_thesis: ( p1 <> p2 implies <*p1,p2*> -: p2 = <*p1,p2*> ) assume A1: p1 <> p2 ; ::_thesis: <*p1,p2*> -: p2 = <*p1,p2*> rng <*p1,p2*> = {p1,p2} by Lm1; then p2 in rng <*p1,p2*> by TARSKI:def_2; hence <*p1,p2*> -: p2 = (<*p1,p2*> -| p2) ^ <*p2*> by Th40 .= <*p1*> ^ <*p2*> by A1, Th26 .= <*p1,p2*> by FINSEQ_1:def_9 ; ::_thesis: verum end; theorem Th50: :: FINSEQ_6:50 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> -: p2 = <*p1,p2*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> -: p2 = <*p1,p2*> let p1, p2, p3 be Element of D; ::_thesis: ( p1 <> p2 implies <*p1,p2,p3*> -: p2 = <*p1,p2*> ) assume A1: p1 <> p2 ; ::_thesis: <*p1,p2,p3*> -: p2 = <*p1,p2*> rng <*p1,p2,p3*> = {p1,p2,p3} by Lm2; then p2 in rng <*p1,p2,p3*> by ENUMSET1:def_1; hence <*p1,p2,p3*> -: p2 = (<*p1,p2,p3*> -| p2) ^ <*p2*> by Th40 .= <*p1*> ^ <*p2*> by A1, Th27 .= <*p1,p2*> by FINSEQ_1:def_9 ; ::_thesis: verum end; theorem Th51: :: FINSEQ_6:51 for D being non empty set for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> -: p3 = <*p1,p2,p3*> proof let D be non empty set ; ::_thesis: for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> -: p3 = <*p1,p2,p3*> let p1, p3, p2 be Element of D; ::_thesis: ( p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*> -: p3 = <*p1,p2,p3*> ) assume that A1: p1 <> p3 and A2: p2 <> p3 ; ::_thesis: <*p1,p2,p3*> -: p3 = <*p1,p2,p3*> rng <*p1,p2,p3*> = {p1,p2,p3} by Lm2; then p3 in rng <*p1,p2,p3*> by ENUMSET1:def_1; hence <*p1,p2,p3*> -: p3 = (<*p1,p2,p3*> -| p3) ^ <*p3*> by Th40 .= <*p1,p2*> ^ <*p3*> by A1, A2, Th28 .= <*p1,p2,p3*> by FINSEQ_1:43 ; ::_thesis: verum end; theorem :: FINSEQ_6:52 for D being non empty set for p being Element of D holds ( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> ) proof let D be non empty set ; ::_thesis: for p being Element of D holds ( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> ) let p be Element of D; ::_thesis: ( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> ) p in {p} by TARSKI:def_1; then A1: p in rng <*p*> by FINSEQ_1:39; hence <*p*> :- p = <*p*> ^ (<*p*> |-- p) by Th41 .= <*p*> ^ {} by Th32 .= <*p*> by FINSEQ_1:34 ; ::_thesis: <*p*> -: p = <*p*> thus <*p*> -: p = (<*p*> -| p) ^ <*p*> by A1, Th40 .= {} ^ <*p*> by Th32 .= <*p*> by FINSEQ_1:34 ; ::_thesis: verum end; theorem Th53: :: FINSEQ_6:53 for D being non empty set for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> :- p2 = <*p2*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> :- p2 = <*p2*> let p1, p2 be Element of D; ::_thesis: ( p1 <> p2 implies <*p1,p2*> :- p2 = <*p2*> ) assume A1: p1 <> p2 ; ::_thesis: <*p1,p2*> :- p2 = <*p2*> p2 in {p1,p2} by TARSKI:def_2; then p2 in rng <*p1,p2*> by Lm1; hence <*p1,p2*> :- p2 = <*p2*> ^ (<*p1,p2*> |-- p2) by Th41 .= <*p2*> ^ {} by A1, Th33 .= <*p2*> by FINSEQ_1:34 ; ::_thesis: verum end; theorem Th54: :: FINSEQ_6:54 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> :- p2 = <*p2,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> :- p2 = <*p2,p3*> let p1, p2, p3 be Element of D; ::_thesis: ( p1 <> p2 implies <*p1,p2,p3*> :- p2 = <*p2,p3*> ) assume A1: p1 <> p2 ; ::_thesis: <*p1,p2,p3*> :- p2 = <*p2,p3*> p2 in {p1,p2,p3} by ENUMSET1:def_1; then p2 in rng <*p1,p2,p3*> by Lm2; hence <*p1,p2,p3*> :- p2 = <*p2*> ^ (<*p1,p2,p3*> |-- p2) by Th41 .= <*p2*> ^ <*p3*> by A1, Th30 .= <*p2,p3*> by FINSEQ_1:def_9 ; ::_thesis: verum end; theorem Th55: :: FINSEQ_6:55 for D being non empty set for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> :- p3 = <*p3*> proof let D be non empty set ; ::_thesis: for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> :- p3 = <*p3*> let p1, p3, p2 be Element of D; ::_thesis: ( p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*> :- p3 = <*p3*> ) assume that A1: p1 <> p3 and A2: p2 <> p3 ; ::_thesis: <*p1,p2,p3*> :- p3 = <*p3*> p3 in {p1,p2,p3} by ENUMSET1:def_1; then p3 in rng <*p1,p2,p3*> by Lm2; hence <*p1,p2,p3*> :- p3 = <*p3*> ^ (<*p1,p2,p3*> |-- p3) by Th41 .= <*p3*> ^ {} by A1, A2, Th34 .= <*p3*> by FINSEQ_1:34 ; ::_thesis: verum end; theorem Th56: :: FINSEQ_6:56 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p .. f = k + (p .. (f /^ k)) proof let k be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p .. f = k + (p .. (f /^ k)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p .. f = k + (p .. (f /^ k)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f > k holds p .. f = k + (p .. (f /^ k)) let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f > k implies p .. f = k + (p .. (f /^ k)) ) assume that A1: p in rng f and A2: p .. f > k ; ::_thesis: p .. f = k + (p .. (f /^ k)) reconsider i = (p .. f) - k as Element of NAT by A2, INT_1:5; A3: i + k <= len f by A1, FINSEQ_4:21; then A4: i <= (len f) - k by XREAL_1:19; k <= k + i by NAT_1:11; then k <= len f by A3, XXREAL_0:2; then A5: i <= len (f /^ k) by A4, RFINSEQ:def_1; i <> 0 by A2; then 1 <= i by NAT_1:14; then A6: i in dom (f /^ k) by A5, FINSEQ_3:25; A7: k + i = p .. f ; A8: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<_i_holds_ (f_/^_k)_/._j_<>_(f_/^_k)_/._i let j be Nat; ::_thesis: ( 1 <= j & j < i implies (f /^ k) /. j <> (f /^ k) /. i ) assume that A9: 1 <= j and A10: j < i ; ::_thesis: (f /^ k) /. j <> (f /^ k) /. i reconsider J = j as Element of NAT by ORDINAL1:def_12; k + j >= j by NAT_1:11; then A11: 1 <= k + j by A9, XXREAL_0:2; j <= len (f /^ k) by A5, A10, XXREAL_0:2; then j in dom (f /^ k) by A9, FINSEQ_3:25; then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:27; A13: k + i <= len f by A1, FINSEQ_4:21; k + j < k + i by A10, XREAL_1:6; then k + j <= len f by A13, XXREAL_0:2; then A14: k + J in dom f by A11, FINSEQ_3:25; k + j < p .. f by A7, A10, XREAL_1:6; then A15: f /. (k + j) <> p by A14, FINSEQ_5:39; f /. (k + i) = (f /^ k) /. i by A6, FINSEQ_5:27; hence (f /^ k) /. j <> (f /^ k) /. i by A1, A12, A15, FINSEQ_5:38; ::_thesis: verum end; (f /^ k) /. i = f /. (k + i) by A6, FINSEQ_5:27 .= p by A1, FINSEQ_5:38 ; then (p .. f) - k = p .. (f /^ k) by A6, A8, Th48; hence p .. f = k + (p .. (f /^ k)) ; ::_thesis: verum end; theorem Th57: :: FINSEQ_6:57 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p in rng (f /^ k) proof let k be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p in rng (f /^ k) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p in rng (f /^ k) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f > k holds p in rng (f /^ k) let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f > k implies p in rng (f /^ k) ) assume that A1: p in rng f and A2: p .. f > k ; ::_thesis: p in rng (f /^ k) A3: k + (p .. (f /^ k)) = p .. f by A1, A2, Th56; then p .. (f /^ k) <> 0 by A2; then A4: 1 <= p .. (f /^ k) by NAT_1:14; p .. f <= len f by A1, FINSEQ_4:21; then k <= len f by A2, XXREAL_0:2; then len (f /^ k) = (len f) - k by RFINSEQ:def_1; then A5: (len (f /^ k)) + k = len f ; k + (p .. (f /^ k)) <= len f by A1, A3, FINSEQ_4:21; then p .. (f /^ k) <= len (f /^ k) by A5, XREAL_1:6; then A6: p .. (f /^ k) in dom (f /^ k) by A4, FINSEQ_3:25; then (f /^ k) /. (p .. (f /^ k)) in rng (f /^ k) by PARTFUN2:2; then f /. (k + (p .. (f /^ k))) in rng (f /^ k) by A6, FINSEQ_5:27; hence p in rng (f /^ k) by A1, A3, FINSEQ_5:38; ::_thesis: verum end; theorem Th58: :: FINSEQ_6:58 for k, i being Nat for D being non empty set for f being FinSequence of D st k < i & i in dom f holds f /. i in rng (f /^ k) proof let k, i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st k < i & i in dom f holds f /. i in rng (f /^ k) let D be non empty set ; ::_thesis: for f being FinSequence of D st k < i & i in dom f holds f /. i in rng (f /^ k) let f be FinSequence of D; ::_thesis: ( k < i & i in dom f implies f /. i in rng (f /^ k) ) assume that A1: k < i and A2: i in dom f ; ::_thesis: f /. i in rng (f /^ k) reconsider j = i - k as Element of NAT by A1, INT_1:5; j > 0 by A1, XREAL_1:50; then A3: 1 <= j by NAT_1:14; A4: i = j + k ; A5: i <= len f by A2, FINSEQ_3:25; then k <= len f by A1, XXREAL_0:2; then len (f /^ k) = (len f) - k by RFINSEQ:def_1; then (len (f /^ k)) + k = len f ; then j <= len (f /^ k) by A4, A5, XREAL_1:6; then A6: j in dom (f /^ k) by A3, FINSEQ_3:25; then f /. i = (f /^ k) /. j by A4, FINSEQ_5:27; hence f /. i in rng (f /^ k) by A6, PARTFUN2:2; ::_thesis: verum end; theorem Th59: :: FINSEQ_6:59 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) -: p = (f -: p) /^ k proof let k be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) -: p = (f -: p) /^ k let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) -: p = (f -: p) /^ k let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) -: p = (f -: p) /^ k let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f > k implies (f /^ k) -: p = (f -: p) /^ k ) assume that A1: p in rng f and A2: p .. f > k ; ::_thesis: (f /^ k) -: p = (f -: p) /^ k A3: p in rng (f /^ k) by A1, A2, Th57; p .. f = k + (p .. (f /^ k)) by A1, A2, Th56; then A4: len ((f /^ k) -: p) = (p .. f) - k by A3, FINSEQ_5:42 .= (len (f -: p)) - k by A1, FINSEQ_5:42 ; A5: now__::_thesis:_for_m_being_Nat_st_m_in_dom_((f_/^_k)_-:_p)_holds_ ((f_/^_k)_-:_p)_._m_=_(f_-:_p)_._(m_+_k) let m be Nat; ::_thesis: ( m in dom ((f /^ k) -: p) implies ((f /^ k) -: p) . m = (f -: p) . (m + k) ) A6: m + k >= m by NAT_1:11; reconsider M = m as Element of NAT by ORDINAL1:def_12; assume A7: m in dom ((f /^ k) -: p) ; ::_thesis: ((f /^ k) -: p) . m = (f -: p) . (m + k) then m <= (len (f -: p)) - k by A4, FINSEQ_3:25; then A8: m + k <= len (f -: p) by XREAL_1:19; 1 <= m by A7, FINSEQ_3:25; then 1 <= m + k by A6, XXREAL_0:2; then A9: M + k in dom (f -: p) by A8, FINSEQ_3:25; len ((f /^ k) -: p) = p .. (f /^ k) by A3, FINSEQ_5:42; then A10: m in Seg (p .. (f /^ k)) by A7, FINSEQ_1:def_3; (f /^ k) -: p = (f /^ k) | (p .. (f /^ k)) by FINSEQ_5:def_1; then A11: dom ((f /^ k) -: p) c= dom (f /^ k) by FINSEQ_5:18; len (f -: p) = p .. f by A1, FINSEQ_5:42; then A12: m + k in Seg (p .. f) by A9, FINSEQ_1:def_3; thus ((f /^ k) -: p) . m = ((f /^ k) -: p) /. m by A7, PARTFUN1:def_6 .= (f /^ k) /. m by A3, A10, FINSEQ_5:43 .= f /. (m + k) by A7, A11, FINSEQ_5:27 .= (f -: p) /. (M + k) by A1, A12, FINSEQ_5:43 .= (f -: p) . (m + k) by A9, PARTFUN1:def_6 ; ::_thesis: verum end; k <= len (f -: p) by A1, A2, FINSEQ_5:42; hence (f /^ k) -: p = (f -: p) /^ k by A4, A5, RFINSEQ:def_1; ::_thesis: verum end; theorem Th60: :: FINSEQ_6:60 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) -: p = (f -: p) /^ 1 proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) -: p = (f -: p) /^ 1 let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) -: p = (f -: p) /^ 1 let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f <> 1 implies (f /^ 1) -: p = (f -: p) /^ 1 ) assume that A1: p in rng f and A2: p .. f <> 1 ; ::_thesis: (f /^ 1) -: p = (f -: p) /^ 1 p .. f >= 1 by A1, FINSEQ_4:21; then p .. f > 1 by A2, XXREAL_0:1; hence (f /^ 1) -: p = (f -: p) /^ 1 by A1, Th59; ::_thesis: verum end; theorem Th61: :: FINSEQ_6:61 for D being non empty set for p being Element of D for f being FinSequence of D holds p in rng (f :- p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds p in rng (f :- p) let p be Element of D; ::_thesis: for f being FinSequence of D holds p in rng (f :- p) let f be FinSequence of D; ::_thesis: p in rng (f :- p) rng <*p*> = {p} by FINSEQ_1:39; then A1: p in rng <*p*> by TARSKI:def_1; f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def_2; then rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31; hence p in rng (f :- p) by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th62: :: FINSEQ_6:62 for x being set for D being non empty set for p being Element of D for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds x in rng (f :- p) proof let x be set ; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds x in rng (f :- p) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds x in rng (f :- p) let p be Element of D; ::_thesis: for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds x in rng (f :- p) let f be FinSequence of D; ::_thesis: ( x in rng f & p in rng f & x .. f >= p .. f implies x in rng (f :- p) ) assume that A1: x in rng f and A2: p in rng f and A3: x .. f >= p .. f ; ::_thesis: x in rng (f :- p) percases ( x .. f > p .. f or x .. f = p .. f ) by A3, XXREAL_0:1; supposeA4: x .. f > p .. f ; ::_thesis: x in rng (f :- p) rng f c= D by FINSEQ_1:def_4; then reconsider q = x as Element of D by A1; f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def_2; then A5: rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31; q in rng (f /^ (p .. f)) by A1, A4, Th57; hence x in rng (f :- p) by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose x .. f = p .. f ; ::_thesis: x in rng (f :- p) then x = f . (p .. f) by A1, FINSEQ_4:19 .= p by A2, FINSEQ_4:19 ; hence x in rng (f :- p) by Th61; ::_thesis: verum end; end; end; theorem Th63: :: FINSEQ_6:63 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds f /. k in rng (f :- p) proof let k be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds f /. k in rng (f :- p) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds f /. k in rng (f :- p) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds f /. k in rng (f :- p) let f be FinSequence of D; ::_thesis: ( p in rng f & k <= len f & k >= p .. f implies f /. k in rng (f :- p) ) assume that A1: p in rng f and A2: k <= len f and A3: k >= p .. f ; ::_thesis: f /. k in rng (f :- p) set x = f /. k; percases ( k > p .. f or k = p .. f ) by A3, XXREAL_0:1; supposeA4: k > p .. f ; ::_thesis: f /. k in rng (f :- p) reconsider q = f /. k as Element of D ; 1 <= p .. f by A1, FINSEQ_4:21; then 1 <= k by A3, XXREAL_0:2; then k in dom f by A2, FINSEQ_3:25; then A5: q in rng (f /^ (p .. f)) by A4, Th58; f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def_2; then rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31; hence f /. k in rng (f :- p) by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose k = p .. f ; ::_thesis: f /. k in rng (f :- p) then f /. k = p by A1, FINSEQ_5:38; hence f /. k in rng (f :- p) by Th61; ::_thesis: verum end; end; end; theorem Th64: :: FINSEQ_6:64 for D being non empty set for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) :- p = (f1 :- p) ^ f2 proof let D be non empty set ; ::_thesis: for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) :- p = (f1 :- p) ^ f2 let p be Element of D; ::_thesis: for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) :- p = (f1 :- p) ^ f2 let f1, f2 be FinSequence of D; ::_thesis: ( p in rng f1 implies (f1 ^ f2) :- p = (f1 :- p) ^ f2 ) assume A1: p in rng f1 ; ::_thesis: (f1 ^ f2) :- p = (f1 :- p) ^ f2 rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; hence (f1 ^ f2) :- p = <*p*> ^ ((f1 ^ f2) |-- p) by Th41 .= <*p*> ^ ((f1 |-- p) ^ f2) by A1, Th8 .= (<*p*> ^ (f1 |-- p)) ^ f2 by FINSEQ_1:32 .= (f1 :- p) ^ f2 by A1, Th41 ; ::_thesis: verum end; theorem Th65: :: FINSEQ_6:65 for D being non empty set for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) :- p = f2 :- p proof let D be non empty set ; ::_thesis: for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) :- p = f2 :- p let p be Element of D; ::_thesis: for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) :- p = f2 :- p let f2, f1 be FinSequence of D; ::_thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) :- p = f2 :- p ) assume A1: p in (rng f2) \ (rng f1) ; ::_thesis: (f1 ^ f2) :- p = f2 :- p rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; hence (f1 ^ f2) :- p = <*p*> ^ ((f1 ^ f2) |-- p) by Th41 .= <*p*> ^ (f2 |-- p) by A1, Th9 .= f2 :- p by A1, Th41 ; ::_thesis: verum end; theorem Th66: :: FINSEQ_6:66 for D being non empty set for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) -: p = f1 -: p proof let D be non empty set ; ::_thesis: for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) -: p = f1 -: p let p be Element of D; ::_thesis: for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) -: p = f1 -: p let f1, f2 be FinSequence of D; ::_thesis: ( p in rng f1 implies (f1 ^ f2) -: p = f1 -: p ) assume A1: p in rng f1 ; ::_thesis: (f1 ^ f2) -: p = f1 -: p rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; hence (f1 ^ f2) -: p = ((f1 ^ f2) -| p) ^ <*p*> by Th40 .= (f1 -| p) ^ <*p*> by A1, Th12 .= f1 -: p by A1, Th40 ; ::_thesis: verum end; theorem Th67: :: FINSEQ_6:67 for D being non empty set for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -: p = f1 ^ (f2 -: p) proof let D be non empty set ; ::_thesis: for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -: p = f1 ^ (f2 -: p) let p be Element of D; ::_thesis: for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -: p = f1 ^ (f2 -: p) let f2, f1 be FinSequence of D; ::_thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) -: p = f1 ^ (f2 -: p) ) assume A1: p in (rng f2) \ (rng f1) ; ::_thesis: (f1 ^ f2) -: p = f1 ^ (f2 -: p) rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then p in rng (f1 ^ f2) by A1, XBOOLE_0:def_3; hence (f1 ^ f2) -: p = ((f1 ^ f2) -| p) ^ <*p*> by Th40 .= (f1 ^ (f2 -| p)) ^ <*p*> by A1, Th15 .= f1 ^ ((f2 -| p) ^ <*p*>) by FINSEQ_1:32 .= f1 ^ (f2 -: p) by A1, Th40 ; ::_thesis: verum end; theorem :: FINSEQ_6:68 for D being non empty set for p being Element of D for f being FinSequence of D holds (f :- p) :- p = f :- p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds (f :- p) :- p = f :- p let p be Element of D; ::_thesis: for f being FinSequence of D holds (f :- p) :- p = f :- p let f be FinSequence of D; ::_thesis: (f :- p) :- p = f :- p A1: (<*p*> ^ (f /^ (p .. f))) /. 1 = p by FINSEQ_5:15; thus (f :- p) :- p = (<*p*> ^ (f /^ (p .. f))) :- p by FINSEQ_5:def_2 .= <*p*> ^ (f /^ (p .. f)) by A1, Th44 .= f :- p by FINSEQ_5:def_2 ; ::_thesis: verum end; theorem Th69: :: FINSEQ_6:69 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds f |-- p2 = (f |-- p1) |-- p2 proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds f |-- p2 = (f |-- p1) |-- p2 let p1, p2 be Element of D; ::_thesis: for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds f |-- p2 = (f |-- p1) |-- p2 let f be FinSequence of D; ::_thesis: ( p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) implies f |-- p2 = (f |-- p1) |-- p2 ) assume that A1: p1 in rng f and A2: p2 in (rng f) \ (rng (f -: p1)) ; ::_thesis: f |-- p2 = (f |-- p1) |-- p2 not p2 in rng (f -: p1) by A2, XBOOLE_0:def_5; then A3: not p2 in rng ((f -| p1) ^ <*p1*>) by A1, Th40; f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:51; then rng f = (rng ((f -| p1) ^ <*p1*>)) \/ (rng (f |-- p1)) by FINSEQ_1:31; then p2 in rng (f |-- p1) by A2, A3, XBOOLE_0:def_3; then A4: p2 in (rng (f |-- p1)) \ (rng ((f -| p1) ^ <*p1*>)) by A3, XBOOLE_0:def_5; thus f |-- p2 = (((f -| p1) ^ <*p1*>) ^ (f |-- p1)) |-- p2 by A1, FINSEQ_4:51 .= (f |-- p1) |-- p2 by A4, Th9 ; ::_thesis: verum end; theorem Th70: :: FINSEQ_6:70 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds rng f = (rng (f -: p)) \/ (rng (f :- p)) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds rng f = (rng (f -: p)) \/ (rng (f :- p)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds rng f = (rng (f -: p)) \/ (rng (f :- p)) let f be FinSequence of D; ::_thesis: ( p in rng f implies rng f = (rng (f -: p)) \/ (rng (f :- p)) ) assume A1: p in rng f ; ::_thesis: rng f = (rng (f -: p)) \/ (rng (f :- p)) then f -: p = (f -| p) ^ <*p*> by Th40; then A2: rng (f -: p) = (rng (f -| p)) \/ (rng <*p*>) by FINSEQ_1:31; f :- p = <*p*> ^ (f |-- p) by A1, Th41; then A3: rng (f :- p) = (rng <*p*>) \/ (rng (f |-- p)) by FINSEQ_1:31; f = ((f -| p) ^ <*p*>) ^ (f |-- p) by A1, FINSEQ_4:51; hence rng f = (rng ((f -| p) ^ <*p*>)) \/ (rng (f |-- p)) by FINSEQ_1:31 .= ((rng (f -| p)) \/ ((rng <*p*>) \/ (rng <*p*>))) \/ (rng (f |-- p)) by FINSEQ_1:31 .= (((rng (f -| p)) \/ (rng <*p*>)) \/ (rng <*p*>)) \/ (rng (f |-- p)) by XBOOLE_1:4 .= (rng (f -: p)) \/ (rng (f :- p)) by A2, A3, XBOOLE_1:4 ; ::_thesis: verum end; theorem Th71: :: FINSEQ_6:71 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds (f :- p1) :- p2 = f :- p2 proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds (f :- p1) :- p2 = f :- p2 let p1, p2 be Element of D; ::_thesis: for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds (f :- p1) :- p2 = f :- p2 let f be FinSequence of D; ::_thesis: ( p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) implies (f :- p1) :- p2 = f :- p2 ) assume that A1: p1 in rng f and A2: p2 in (rng f) \ (rng (f -: p1)) ; ::_thesis: (f :- p1) :- p2 = f :- p2 A3: not p2 in rng (f -: p1) by A2, XBOOLE_0:def_5; f -: p1 = (f -| p1) ^ <*p1*> by A1, Th40; then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31; then A4: not p2 in rng <*p1*> by A3, XBOOLE_0:def_3; rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A1, Th70; then A5: p2 in rng (f :- p1) by A2, A3, XBOOLE_0:def_3; f :- p1 = <*p1*> ^ (f |-- p1) by A1, Th41; then rng (f :- p1) = (rng <*p1*>) \/ (rng (f |-- p1)) by FINSEQ_1:31; then p2 in rng (f |-- p1) by A5, A4, XBOOLE_0:def_3; then A6: p2 in (rng (f |-- p1)) \ (rng <*p1*>) by A4, XBOOLE_0:def_5; thus (f :- p1) :- p2 = <*p2*> ^ ((f :- p1) |-- p2) by A5, Th41 .= <*p2*> ^ ((<*p1*> ^ (f |-- p1)) |-- p2) by A1, Th41 .= <*p2*> ^ ((f |-- p1) |-- p2) by A6, Th9 .= <*p2*> ^ (f |-- p2) by A1, A2, Th69 .= f :- p2 by A2, Th41 ; ::_thesis: verum end; theorem Th72: :: FINSEQ_6:72 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds p .. (f -: p) = p .. f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds p .. (f -: p) = p .. f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds p .. (f -: p) = p .. f let f be FinSequence of D; ::_thesis: ( p in rng f implies p .. (f -: p) = p .. f ) assume A1: p in rng f ; ::_thesis: p .. (f -: p) = p .. f then A2: p .. f <= len (f -: p) by FINSEQ_5:42; A3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<_p_.._f_holds_ (f_-:_p)_/._i_<>_(f_-:_p)_/._(p_.._f) p .. f <> 0 by A1, FINSEQ_4:21; then p .. f in Seg (p .. f) by FINSEQ_1:3; then A4: (f -: p) /. (p .. f) = f /. (p .. f) by A1, FINSEQ_5:43; let i be Nat; ::_thesis: ( 1 <= i & i < p .. f implies (f -: p) /. i <> (f -: p) /. (p .. f) ) assume that A5: 1 <= i and A6: i < p .. f ; ::_thesis: (f -: p) /. i <> (f -: p) /. (p .. f) i in Seg (p .. f) by A5, A6, FINSEQ_1:1; then A7: (f -: p) /. i = f /. i by A1, FINSEQ_5:43; p .. f <= len f by A1, FINSEQ_4:21; then i <= len f by A6, XXREAL_0:2; then A8: i in dom f by A5, FINSEQ_3:25; f /. (p .. f) = p by A1, FINSEQ_5:38; hence (f -: p) /. i <> (f -: p) /. (p .. f) by A6, A7, A4, A8, FINSEQ_5:39; ::_thesis: verum end; 1 <= p .. f by A1, FINSEQ_4:21; then A9: p .. f in dom (f -: p) by A2, FINSEQ_3:25; (f -: p) /. (p .. f) = p by A1, FINSEQ_5:45; hence p .. (f -: p) = p .. f by A9, A3, Th48; ::_thesis: verum end; theorem Th73: :: FINSEQ_6:73 for i being Nat for D being non empty set for f being FinSequence of D holds (f | i) | i = f | i proof let i be Nat; ::_thesis: for D being non empty set for f being FinSequence of D holds (f | i) | i = f | i let D be non empty set ; ::_thesis: for f being FinSequence of D holds (f | i) | i = f | i let f be FinSequence of D; ::_thesis: (f | i) | i = f | i f | i = f | (Seg i) by FINSEQ_1:def_15; hence (f | i) | i = (f | (Seg i)) | (Seg i) by FINSEQ_1:def_15 .= f | ((Seg i) /\ (Seg i)) .= f | i by FINSEQ_1:def_15 ; ::_thesis: verum end; theorem Th74: :: FINSEQ_6:74 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) -: p = f -: p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) -: p = f -: p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (f -: p) -: p = f -: p let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -: p) -: p = f -: p ) assume p in rng f ; ::_thesis: (f -: p) -: p = f -: p then A1: p .. (f -: p) = p .. f by Th72; thus (f -: p) -: p = (f -: p) | (p .. (f -: p)) by FINSEQ_5:def_1 .= (f | (p .. f)) | (p .. f) by A1, FINSEQ_5:def_1 .= f | (p .. f) by Th73 .= f -: p by FINSEQ_5:def_1 ; ::_thesis: verum end; theorem Th75: :: FINSEQ_6:75 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds (f -: p1) -: p2 = f -: p2 proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds (f -: p1) -: p2 = f -: p2 let p1, p2 be Element of D; ::_thesis: for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds (f -: p1) -: p2 = f -: p2 let f be FinSequence of D; ::_thesis: ( p1 in rng f & p2 in rng (f -: p1) implies (f -: p1) -: p2 = f -: p2 ) assume that A1: p1 in rng f and A2: p2 in rng (f -: p1) ; ::_thesis: (f -: p1) -: p2 = f -: p2 percases ( p1 = p2 or p1 <> p2 ) ; suppose p1 = p2 ; ::_thesis: (f -: p1) -: p2 = f -: p2 hence (f -: p1) -: p2 = f -: p2 by A1, Th74; ::_thesis: verum end; suppose p1 <> p2 ; ::_thesis: (f -: p1) -: p2 = f -: p2 then not p2 in {p1} by TARSKI:def_1; then A3: not p2 in rng <*p1*> by FINSEQ_1:39; f -: p1 = (f -| p1) ^ <*p1*> by A1, Th40; then rng (f -: p1) = (rng (f -| p1)) \/ (rng <*p1*>) by FINSEQ_1:31; then A4: p2 in rng (f -| p1) by A2, A3, XBOOLE_0:def_3; A5: rng (f -| p1) c= rng f by A1, FINSEQ_4:39; thus (f -: p1) -: p2 = ((f -: p1) -| p2) ^ <*p2*> by A2, Th40 .= (((f -| p1) ^ <*p1*>) -| p2) ^ <*p2*> by A1, Th40 .= ((f -| p1) -| p2) ^ <*p2*> by A4, Th12 .= (f -| p2) ^ <*p2*> by A1, A4, Th35 .= f -: p2 by A4, A5, Th40 ; ::_thesis: verum end; end; end; theorem Th76: :: FINSEQ_6:76 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) ^ ((f :- p) /^ 1) = f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) ^ ((f :- p) /^ 1) = f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (f -: p) ^ ((f :- p) /^ 1) = f let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -: p) ^ ((f :- p) /^ 1) = f ) A1: rng f c= D by FINSEQ_1:def_4; assume A2: p in rng f ; ::_thesis: (f -: p) ^ ((f :- p) /^ 1) = f then rng (f |-- p) c= rng f by FINSEQ_4:44; then rng (f |-- p) c= D by A1, XBOOLE_1:1; then reconsider f1 = f |-- p as FinSequence of D by FINSEQ_1:def_4; thus (f -: p) ^ ((f :- p) /^ 1) = ((f -| p) ^ <*p*>) ^ ((f :- p) /^ 1) by A2, Th40 .= ((f -| p) ^ <*p*>) ^ ((<*p*> ^ f1) /^ 1) by A2, Th41 .= ((f -| p) ^ <*p*>) ^ (f |-- p) by Th45 .= f by A2, FINSEQ_4:51 ; ::_thesis: verum end; theorem Th77: :: FINSEQ_6:77 for D being non empty set for f1, f2 being FinSequence of D st f1 <> {} holds (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 proof let D be non empty set ; ::_thesis: for f1, f2 being FinSequence of D st f1 <> {} holds (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 let f1, f2 be FinSequence of D; ::_thesis: ( f1 <> {} implies (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 ) assume f1 <> {} ; ::_thesis: (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 then consider p being Element of D, df1 being FinSequence of D such that p = f1 . 1 and A1: f1 = <*p*> ^ df1 by FINSEQ_3:102; thus (f1 ^ f2) /^ 1 = (<*p*> ^ (df1 ^ f2)) /^ 1 by A1, FINSEQ_1:32 .= df1 ^ f2 by Th45 .= (f1 /^ 1) ^ f2 by A1, Th45 ; ::_thesis: verum end; theorem Th78: :: FINSEQ_6:78 for D being non empty set for p2 being Element of D for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds p2 in rng (f /^ 1) proof let D be non empty set ; ::_thesis: for p2 being Element of D for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds p2 in rng (f /^ 1) let p2 be Element of D; ::_thesis: for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds p2 in rng (f /^ 1) let f be FinSequence of D; ::_thesis: ( p2 in rng f & p2 .. f <> 1 implies p2 in rng (f /^ 1) ) assume that A1: p2 in rng f and A2: p2 .. f <> 1 ; ::_thesis: p2 in rng (f /^ 1) f = <*(f /. 1)*> ^ (f /^ 1) by A1, FINSEQ_5:29, RELAT_1:38; then A3: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31; assume not p2 in rng (f /^ 1) ; ::_thesis: contradiction then p2 in rng <*(f /. 1)*> by A1, A3, XBOOLE_0:def_3; then p2 in {(f /. 1)} by FINSEQ_1:39; then p2 = f /. 1 by TARSKI:def_1; hence contradiction by A1, A2, Th43, RELAT_1:38; ::_thesis: verum end; theorem Th79: :: FINSEQ_6:79 for D being non empty set for p being Element of D for f being FinSequence of D holds p .. (f :- p) = 1 proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds p .. (f :- p) = 1 let p be Element of D; ::_thesis: for f being FinSequence of D holds p .. (f :- p) = 1 let f be FinSequence of D; ::_thesis: p .. (f :- p) = 1 (f :- p) /. 1 = p by FINSEQ_5:53; hence p .. (f :- p) = 1 by Th43; ::_thesis: verum end; Lm3: for i being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > i holds i + (p .. (f /^ i)) = p .. f proof let i be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > i holds i + (p .. (f /^ i)) = p .. f let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f > i holds i + (p .. (f /^ i)) = p .. f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f > i holds i + (p .. (f /^ i)) = p .. f let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f > i implies i + (p .. (f /^ i)) = p .. f ) assume that A1: p in rng f and A2: p .. f > i ; ::_thesis: i + (p .. (f /^ i)) = p .. f reconsider k = (p .. f) - i as Element of NAT by A2, INT_1:5; A3: p .. f <= len f by A1, FINSEQ_4:21; then A4: i <= len f by A2, XXREAL_0:2; (p .. f) - i <= (len f) - i by A3, XREAL_1:9; then A5: k <= len (f /^ i) by A4, RFINSEQ:def_1; k <> 0 by A2; then 1 <= k by NAT_1:14; then A6: k in dom (f /^ i) by A5, FINSEQ_3:25; A7: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<_k_holds_ (f_/^_i)_._j_<>_(f_/^_i)_._k let j be Nat; ::_thesis: ( 1 <= j & j < k implies (f /^ i) . j <> (f /^ i) . k ) assume that A8: 1 <= j and A9: j < k ; ::_thesis: (f /^ i) . j <> (f /^ i) . k j <= i + j by NAT_1:11; then A10: 1 <= i + j by A8, XXREAL_0:2; i + k = p .. f ; then A11: i + j < p .. f by A9, XREAL_1:6; then i + j <= len f by A3, XXREAL_0:2; then A12: i + j in dom f by A10, FINSEQ_3:25; j <= len (f /^ i) by A5, A9, XXREAL_0:2; then j in dom (f /^ i) by A8, FINSEQ_3:25; then A13: f . (i + j) = (f /^ i) . j by A4, RFINSEQ:def_1; f . (i + k) = (f /^ i) . k by A4, A6, RFINSEQ:def_1; hence (f /^ i) . j <> (f /^ i) . k by A1, A13, A11, A12, FINSEQ_4:19, FINSEQ_4:24; ::_thesis: verum end; (f /^ i) . k = f . (k + i) by A4, A6, RFINSEQ:def_1 .= p by A1, FINSEQ_4:19 ; then p .. (f /^ i) = k by A6, A7, Th2; hence i + (p .. (f /^ i)) = p .. f ; ::_thesis: verum end; theorem Th80: :: FINSEQ_6:80 for k being Nat for D being non empty set holds (<*> D) /^ k = <*> D proof let k be Nat; ::_thesis: for D being non empty set holds (<*> D) /^ k = <*> D let D be non empty set ; ::_thesis: (<*> D) /^ k = <*> D percases ( k = 0 or k > 0 ) ; suppose k = 0 ; ::_thesis: (<*> D) /^ k = <*> D hence (<*> D) /^ k = <*> D by FINSEQ_5:28; ::_thesis: verum end; suppose k > 0 ; ::_thesis: (<*> D) /^ k = <*> D then k > len (<*> D) ; hence (<*> D) /^ k = <*> D by RFINSEQ:def_1; ::_thesis: verum end; end; end; theorem Th81: :: FINSEQ_6:81 for i, k being Nat for D being non empty set for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k proof let i, k be Nat; ::_thesis: for D being non empty set for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k let D be non empty set ; ::_thesis: for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k let f be FinSequence of D; ::_thesis: f /^ (i + k) = (f /^ i) /^ k percases ( i + k <= len f or ( i + k > len f & i <= len f ) or ( i + k > len f & i > len f ) ) ; supposeA1: i + k <= len f ; ::_thesis: f /^ (i + k) = (f /^ i) /^ k i <= i + k by NAT_1:11; then A2: i <= len f by A1, XXREAL_0:2; then A3: len (f /^ i) = (len f) - i by RFINSEQ:def_1; then A4: k <= len (f /^ i) by A1, XREAL_1:19; A5: now__::_thesis:_for_m_being_Nat_st_m_in_dom_((f_/^_i)_/^_k)_holds_ ((f_/^_i)_/^_k)_._m_=_f_._(m_+_(i_+_k)) let m be Nat; ::_thesis: ( m in dom ((f /^ i) /^ k) implies ((f /^ i) /^ k) . m = f . (m + (i + k)) ) assume A6: m in dom ((f /^ i) /^ k) ; ::_thesis: ((f /^ i) /^ k) . m = f . (m + (i + k)) then A7: m + k in dom (f /^ i) by FINSEQ_5:26; thus ((f /^ i) /^ k) . m = (f /^ i) . (m + k) by A4, A6, RFINSEQ:def_1 .= f . ((m + k) + i) by A2, A7, RFINSEQ:def_1 .= f . (m + (i + k)) ; ::_thesis: verum end; len ((f /^ i) /^ k) = (len (f /^ i)) - k by A4, RFINSEQ:def_1 .= (len f) - (i + k) by A3 ; hence f /^ (i + k) = (f /^ i) /^ k by A1, A5, RFINSEQ:def_1; ::_thesis: verum end; supposethat A8: i + k > len f and A9: i <= len f ; ::_thesis: f /^ (i + k) = (f /^ i) /^ k len (f /^ i) = (len f) - i by A9, RFINSEQ:def_1; then (len (f /^ i)) + i = len f ; then A10: k > len (f /^ i) by A8, XREAL_1:6; thus f /^ (i + k) = <*> D by A8, RFINSEQ:def_1 .= (f /^ i) /^ k by A10, RFINSEQ:def_1 ; ::_thesis: verum end; supposethat A11: i + k > len f and A12: i > len f ; ::_thesis: f /^ (i + k) = (f /^ i) /^ k thus f /^ (i + k) = <*> D by A11, RFINSEQ:def_1 .= (<*> D) /^ k by Th80 .= (f /^ i) /^ k by A12, RFINSEQ:def_1 ; ::_thesis: verum end; end; end; theorem Th82: :: FINSEQ_6:82 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) :- p = f :- p proof let k be Nat; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) :- p = f :- p let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) :- p = f :- p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) :- p = f :- p let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f > k implies (f /^ k) :- p = f :- p ) assume that A1: p in rng f and A2: p .. f > k ; ::_thesis: (f /^ k) :- p = f :- p thus (f /^ k) :- p = <*p*> ^ ((f /^ k) /^ (p .. (f /^ k))) by FINSEQ_5:def_2 .= <*p*> ^ (f /^ (k + (p .. (f /^ k)))) by Th81 .= <*p*> ^ (f /^ (p .. f)) by A1, A2, Lm3 .= f :- p by FINSEQ_5:def_2 ; ::_thesis: verum end; theorem Th83: :: FINSEQ_6:83 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) :- p = f :- p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) :- p = f :- p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) :- p = f :- p let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f <> 1 implies (f /^ 1) :- p = f :- p ) assume that A1: p in rng f and A2: p .. f <> 1 ; ::_thesis: (f /^ 1) :- p = f :- p p .. f >= 1 by A1, FINSEQ_4:21; then p .. f > 1 by A2, XXREAL_0:1; hence (f /^ 1) :- p = f :- p by A1, Th82; ::_thesis: verum end; theorem Th84: :: FINSEQ_6:84 for i, k being Nat for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f /^ k) = (Rev f) | i proof let i, k be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f /^ k) = (Rev f) | i let D be non empty set ; ::_thesis: for f being FinSequence of D st i + k = len f holds Rev (f /^ k) = (Rev f) | i let f be FinSequence of D; ::_thesis: ( i + k = len f implies Rev (f /^ k) = (Rev f) | i ) assume A1: i + k = len f ; ::_thesis: Rev (f /^ k) = (Rev f) | i then A2: k <= len f by NAT_1:11; i <= len f by A1, NAT_1:11; then i <= len (Rev f) by FINSEQ_5:def_3; then A3: len ((Rev f) | i) = (len f) - k by A1, FINSEQ_1:59 .= len (f /^ k) by A2, RFINSEQ:def_1 ; now__::_thesis:_for_j_being_Nat_st_j_in_dom_((Rev_f)_|_i)_holds_ ((Rev_f)_|_i)_._j_=_(f_/^_k)_._(((len_(f_/^_k))_-_j)_+_1) A4: len (f /^ k) = (len f) - k by A2, RFINSEQ:def_1; let j be Nat; ::_thesis: ( j in dom ((Rev f) | i) implies ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1) ) A5: dom ((Rev f) | i) c= dom (Rev f) by FINSEQ_5:18; assume A6: j in dom ((Rev f) | i) ; ::_thesis: ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1) then j <= len (f /^ k) by A3, FINSEQ_3:25; then reconsider m = (len (f /^ k)) - j as Element of NAT by INT_1:5; j >= 1 by A6, FINSEQ_3:25; then (len (f /^ k)) - j <= (len (f /^ k)) - 1 by XREAL_1:10; then A7: ((len (f /^ k)) - j) + 1 <= len (f /^ k) by XREAL_1:19; 1 <= m + 1 by NAT_1:11; then A8: m + 1 in dom (f /^ k) by A7, FINSEQ_3:25; thus ((Rev f) | i) . j = ((Rev f) | i) /. j by A6, PARTFUN1:def_6 .= (Rev f) /. j by A6, FINSEQ_4:70 .= (Rev f) . j by A6, A5, PARTFUN1:def_6 .= f . ((((len (f /^ k)) + k) - j) + 1) by A6, A5, A4, FINSEQ_5:def_3 .= f . ((m + 1) + k) .= (f /^ k) . (((len (f /^ k)) - j) + 1) by A2, A8, RFINSEQ:def_1 ; ::_thesis: verum end; hence Rev (f /^ k) = (Rev f) | i by A3, FINSEQ_5:def_3; ::_thesis: verum end; theorem Th85: :: FINSEQ_6:85 for i, k being Nat for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f | k) = (Rev f) /^ i proof let i, k be Nat; ::_thesis: for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f | k) = (Rev f) /^ i let D be non empty set ; ::_thesis: for f being FinSequence of D st i + k = len f holds Rev (f | k) = (Rev f) /^ i let f be FinSequence of D; ::_thesis: ( i + k = len f implies Rev (f | k) = (Rev f) /^ i ) assume i + k = len f ; ::_thesis: Rev (f | k) = (Rev f) /^ i then A1: i + k = len (Rev f) by FINSEQ_5:def_3; thus Rev (f | k) = Rev ((Rev (Rev f)) | k) .= Rev (Rev ((Rev f) /^ i)) by A1, Th84 .= (Rev f) /^ i ; ::_thesis: verum end; theorem Th86: :: FINSEQ_6:86 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f |-- p) = (Rev f) -| p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f |-- p) = (Rev f) -| p let p be Element of D; ::_thesis: for f being FinSequence of D st f just_once_values p holds Rev (f |-- p) = (Rev f) -| p let f be FinSequence of D; ::_thesis: ( f just_once_values p implies Rev (f |-- p) = (Rev f) -| p ) assume A1: f just_once_values p ; ::_thesis: Rev (f |-- p) = (Rev f) -| p then A2: p in rng f by FINSEQ_4:5; then A3: p in rng (Rev f) by FINSEQ_5:57; then reconsider n = (p .. (Rev f)) - 1 as Element of NAT by FINSEQ_4:21, INT_1:5; (p .. f) + (p .. (Rev f)) = (len f) + 1 by A1, Th37; then A4: n + (p .. f) = len f ; Rev (f |-- p) = Rev (f /^ (p .. f)) by A2, FINSEQ_5:35 .= (Rev f) | n by A4, Th84 .= (Rev f) | (Seg n) by FINSEQ_1:def_15 ; hence Rev (f |-- p) = (Rev f) -| p by A3, FINSEQ_4:def_5; ::_thesis: verum end; theorem Th87: :: FINSEQ_6:87 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f :- p) = (Rev f) -: p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f :- p) = (Rev f) -: p let p be Element of D; ::_thesis: for f being FinSequence of D st f just_once_values p holds Rev (f :- p) = (Rev f) -: p let f be FinSequence of D; ::_thesis: ( f just_once_values p implies Rev (f :- p) = (Rev f) -: p ) assume A1: f just_once_values p ; ::_thesis: Rev (f :- p) = (Rev f) -: p then A2: p in rng f by FINSEQ_4:5; then A3: p in rng (Rev f) by FINSEQ_5:57; thus Rev (f :- p) = Rev (<*p*> ^ (f |-- p)) by A2, Th41 .= (Rev (f |-- p)) ^ <*p*> by Th24 .= ((Rev f) -| p) ^ <*p*> by A1, Th86 .= (Rev f) -: p by A3, Th40 ; ::_thesis: verum end; theorem Th88: :: FINSEQ_6:88 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f -: p) = (Rev f) :- p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f -: p) = (Rev f) :- p let p be Element of D; ::_thesis: for f being FinSequence of D st f just_once_values p holds Rev (f -: p) = (Rev f) :- p let f be FinSequence of D; ::_thesis: ( f just_once_values p implies Rev (f -: p) = (Rev f) :- p ) assume A1: f just_once_values p ; ::_thesis: Rev (f -: p) = (Rev f) :- p then A2: p in rng f by FINSEQ_4:5; then A3: p in rng (Rev f) by FINSEQ_5:57; thus Rev (f -: p) = Rev ((f -| p) ^ <*p*>) by A2, Th40 .= <*p*> ^ (Rev (f -| p)) by FINSEQ_5:63 .= <*p*> ^ ((Rev f) |-- p) by A1, Th38 .= (Rev f) :- p by A3, Th41 ; ::_thesis: verum end; begin definition let D be non empty set ; let IT be FinSequence of D; attrIT is circular means :Def1: :: FINSEQ_6:def 1 IT /. 1 = IT /. (len IT); end; :: deftheorem Def1 defines circular FINSEQ_6:def_1_:_ for D being non empty set for IT being FinSequence of D holds ( IT is circular iff IT /. 1 = IT /. (len IT) ); definition let D be non empty set ; let f be FinSequence of D; let p be Element of D; func Rotate (f,p) -> FinSequence of D equals :Def2: :: FINSEQ_6:def 2 (f :- p) ^ ((f -: p) /^ 1) if p in rng f otherwise f; correctness coherence ( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) ); consistency for b1 being FinSequence of D holds verum; ; end; :: deftheorem Def2 defines Rotate FINSEQ_6:def_2_:_ for D being non empty set for f being FinSequence of D for p being Element of D holds ( ( p in rng f implies Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate (f,p) = f ) ); registration let D be non empty set ; let f be non empty FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> non empty ; coherence not Rotate (f,p) is empty proof percases ( p in rng f or not p in rng f ) ; supposeA1: p in rng f ; ::_thesis: not Rotate (f,p) is empty not (f :- p) ^ ((f -: p) /^ 1) is empty ; hence not Rotate (f,p) is empty by A1, Def2; ::_thesis: verum end; suppose not p in rng f ; ::_thesis: not Rotate (f,p) is empty hence not Rotate (f,p) is empty by Def2; ::_thesis: verum end; end; end; end; registration let D be non empty set ; cluster Relation-like NAT -defined D -valued Function-like V34() 1 -element FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is circular & b1 is 1 -element ) proof set d = the Element of D; take <* the Element of D*> ; ::_thesis: ( <* the Element of D*> is circular & <* the Element of D*> is 1 -element ) <* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:39; hence <* the Element of D*> is circular by Def1; ::_thesis: <* the Element of D*> is 1 -element thus <* the Element of D*> is 1 -element ; ::_thesis: verum end; cluster non trivial Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is circular & not b1 is trivial ) proof set d = the Element of D; take <* the Element of D, the Element of D*> ; ::_thesis: ( <* the Element of D, the Element of D*> is circular & not <* the Element of D, the Element of D*> is trivial ) len <* the Element of D, the Element of D*> = 2 by FINSEQ_1:44; then <* the Element of D, the Element of D*> /. (len <* the Element of D, the Element of D*>) = the Element of D by FINSEQ_4:17 .= <* the Element of D, the Element of D*> /. 1 by FINSEQ_4:17 ; hence <* the Element of D, the Element of D*> is circular by Def1; ::_thesis: not <* the Element of D, the Element of D*> is trivial thus not <* the Element of D, the Element of D*> is trivial ; ::_thesis: verum end; end; theorem Th89: :: FINSEQ_6:89 for D being non empty set for f being FinSequence of D holds Rotate (f,(f /. 1)) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D holds Rotate (f,(f /. 1)) = f let f be FinSequence of D; ::_thesis: Rotate (f,(f /. 1)) = f A1: len <*(f /. 1)*> = 1 by FINSEQ_1:39; percases ( not f is empty or f is empty ) ; supposeA2: not f is empty ; ::_thesis: Rotate (f,(f /. 1)) = f then f /. 1 in rng f by Th42; hence Rotate (f,(f /. 1)) = (f :- (f /. 1)) ^ ((f -: (f /. 1)) /^ 1) by Def2 .= f ^ ((f -: (f /. 1)) /^ 1) by A2, Th44 .= f ^ (<*(f /. 1)*> /^ 1) by A2, Th44 .= f ^ {} by A1, FINSEQ_5:32 .= f by FINSEQ_1:34 ; ::_thesis: verum end; suppose f is empty ; ::_thesis: Rotate (f,(f /. 1)) = f hence Rotate (f,(f /. 1)) = f by Def2, RELAT_1:38; ::_thesis: verum end; end; end; registration let D be non empty set ; let p be Element of D; let f be non empty circular FinSequence of D; cluster Rotate (f,p) -> circular ; coherence Rotate (f,p) is circular proof percases ( not p in rng f or ( p in rng f & p <> f /. 1 ) or ( p in rng f & p = f /. 1 ) ) ; suppose not p in rng f ; ::_thesis: Rotate (f,p) is circular hence Rotate (f,p) is circular by Def2; ::_thesis: verum end; supposethat A1: p in rng f and A2: p <> f /. 1 ; ::_thesis: Rotate (f,p) is circular A3: p .. f >= 1 by A1, FINSEQ_4:21; A4: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, Def2; p .. f <> 1 by A1, A2, FINSEQ_5:38; then p .. f > 1 by A3, XXREAL_0:1; then p .. f >= 1 + 1 by NAT_1:13; then A5: len (f -: p) >= 1 + 1 by A1, FINSEQ_5:42; then 1 <= len (f -: p) by XXREAL_0:2; then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def_1; then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ; then len ((f -: p) /^ 1) >= 1 by A5, XREAL_1:6; then A7: len ((f -: p) /^ 1) in dom ((f -: p) /^ 1) by FINSEQ_3:25; 1 in dom (f :- p) by FINSEQ_5:6; hence (Rotate (f,p)) /. 1 = (f :- p) /. 1 by A4, FINSEQ_4:68 .= p by FINSEQ_5:53 .= (f -: p) /. (p .. f) by A1, FINSEQ_5:45 .= (f -: p) /. ((len ((f -: p) /^ 1)) + 1) by A1, A6, FINSEQ_5:42 .= ((f -: p) /^ 1) /. (len ((f -: p) /^ 1)) by A7, FINSEQ_5:27 .= ((f :- p) ^ ((f -: p) /^ 1)) /. ((len (f :- p)) + (len ((f -: p) /^ 1))) by A7, FINSEQ_4:69 .= (Rotate (f,p)) /. (len (Rotate (f,p))) by A4, FINSEQ_1:22 ; :: according to FINSEQ_6:def_1 ::_thesis: verum end; suppose ( p in rng f & p = f /. 1 ) ; ::_thesis: Rotate (f,p) is circular hence Rotate (f,p) is circular by Th89; ::_thesis: verum end; end; end; end; theorem :: FINSEQ_6:90 for D being non empty set for p being Element of D for f being FinSequence of D st f is circular & p in rng f holds rng (Rotate (f,p)) = rng f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f is circular & p in rng f holds rng (Rotate (f,p)) = rng f let p be Element of D; ::_thesis: for f being FinSequence of D st f is circular & p in rng f holds rng (Rotate (f,p)) = rng f let f be FinSequence of D; ::_thesis: ( f is circular & p in rng f implies rng (Rotate (f,p)) = rng f ) assume that A1: f is circular and A2: p in rng f ; ::_thesis: rng (Rotate (f,p)) = rng f A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A2, Def2; A4: rng ((f -: p) /^ 1) c= rng (f -: p) by FINSEQ_5:33; rng (f -: p) c= rng f by FINSEQ_5:48; then A5: rng ((f -: p) /^ 1) c= rng f by A4, XBOOLE_1:1; A6: rng ((f :- p) ^ ((f -: p) /^ 1)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31; rng (f :- p) c= rng f by A2, FINSEQ_5:55; hence rng (Rotate (f,p)) c= rng f by A3, A6, A5, XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: rng f c= rng (Rotate (f,p)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in rng (Rotate (f,p)) ) assume x in rng f ; ::_thesis: x in rng (Rotate (f,p)) then consider i being Nat such that A7: i in dom f and A8: f . i = x by FINSEQ_2:10; A9: x = f /. i by A7, A8, PARTFUN1:def_6; percases ( i = 1 or ( i <= p .. f & i <> 1 ) or i > p .. f ) ; supposeA10: i = 1 ; ::_thesis: x in rng (Rotate (f,p)) len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def_2 .= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22 .= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ; then 1 <= len (f :- p) by NAT_1:11; then A11: len (f :- p) in dom (f :- p) by FINSEQ_3:25; x = f /. (len f) by A1, A9, A10, Def1 .= (f :- p) /. (len (f :- p)) by A2, FINSEQ_5:54 ; then x in rng (f :- p) by A11, PARTFUN2:2; hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def_3; ::_thesis: verum end; supposethat A12: i <= p .. f and A13: i <> 1 ; ::_thesis: x in rng (Rotate (f,p)) A14: i <> 0 by A7, FINSEQ_3:25; then A15: i > 0 + 1 by A13, NAT_1:25; then A16: i in Seg (p .. f) by A12, FINSEQ_1:1; consider j being Nat such that A17: i = j + 1 by A14, NAT_1:6; A18: j >= 1 by A15, A17, NAT_1:14; A19: i <= len (f -: p) by A2, A12, FINSEQ_5:42; then 1 <= len (f -: p) by A14, NAT_1:25, XXREAL_0:2; then len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def_1; then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ; then j <= len ((f -: p) /^ 1) by A17, A19, XREAL_1:6; then A20: j in dom ((f -: p) /^ 1) by A18, FINSEQ_3:25; A21: len <*((f -: p) /. 1)*> = 1 by FINSEQ_1:39; f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by A2, FINSEQ_5:29, FINSEQ_5:47; then ((f -: p) /^ 1) /. j = (f -: p) /. i by A17, A20, A21, FINSEQ_4:69 .= f /. i by A2, A16, FINSEQ_5:43 ; then x in rng ((f -: p) /^ 1) by A9, A20, PARTFUN2:2; hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def_3; ::_thesis: verum end; suppose i > p .. f ; ::_thesis: x in rng (Rotate (f,p)) then reconsider j = i - (p .. f) as Element of NAT by INT_1:5; A22: j + 1 >= 1 by NAT_1:11; i <= len f by A7, FINSEQ_3:25; then A23: j <= (len f) - (p .. f) by XREAL_1:9; len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50; then j + 1 <= len (f :- p) by A23, XREAL_1:6; then A24: j + 1 in dom (f :- p) by A22, FINSEQ_3:25; j + (p .. f) = i ; then f /. i = (f :- p) /. (j + 1) by A2, A24, FINSEQ_5:52; then x in rng (f :- p) by A9, A24, PARTFUN2:2; hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem Th91: :: FINSEQ_6:91 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds p in rng (Rotate (f,p)) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds p in rng (Rotate (f,p)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds p in rng (Rotate (f,p)) let f be FinSequence of D; ::_thesis: ( p in rng f implies p in rng (Rotate (f,p)) ) p in {p} by TARSKI:def_1; then p in rng <*p*> by FINSEQ_1:39; then p in (rng <*p*>) \/ (rng (f /^ (p .. f))) by XBOOLE_0:def_3; then p in rng (<*p*> ^ (f /^ (p .. f))) by FINSEQ_1:31; then A1: p in rng (f :- p) by FINSEQ_5:def_2; assume p in rng f ; ::_thesis: p in rng (Rotate (f,p)) then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2; then rng (Rotate (f,p)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31; hence p in rng (Rotate (f,p)) by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th92: :: FINSEQ_6:92 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. 1 = p proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. 1 = p let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. 1 = p let f be FinSequence of D; ::_thesis: ( p in rng f implies (Rotate (f,p)) /. 1 = p ) assume p in rng f ; ::_thesis: (Rotate (f,p)) /. 1 = p then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2 .= (<*p*> ^ (f /^ (p .. f))) ^ ((f -: p) /^ 1) by FINSEQ_5:def_2 .= <*p*> ^ ((f /^ (p .. f)) ^ ((f -: p) /^ 1)) by FINSEQ_1:32 ; hence (Rotate (f,p)) /. 1 = p by FINSEQ_5:15; ::_thesis: verum end; theorem Th93: :: FINSEQ_6:93 for D being non empty set for p being Element of D for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p) let p be Element of D; ::_thesis: for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p) let f be FinSequence of D; ::_thesis: Rotate ((Rotate (f,p)),p) = Rotate (f,p) percases ( p in rng f or not p in rng f ) ; supposeA1: p in rng f ; ::_thesis: Rotate ((Rotate (f,p)),p) = Rotate (f,p) then reconsider f9 = f as non empty FinSequence of D ; A2: (Rotate (f,p)) /. 1 = p by A1, Th92; then A3: (Rotate (f9,p)) :- p = Rotate (f,p) by Th44; A4: p in rng (Rotate (f,p)) by A1, Th91; A5: len <*p*> = 1 by FINSEQ_1:39; (Rotate (f9,p)) -: p = <*p*> by A2, Th44; hence Rotate ((Rotate (f,p)),p) = (Rotate (f,p)) ^ (<*p*> /^ 1) by A3, A4, Def2 .= (Rotate (f,p)) ^ {} by A5, FINSEQ_5:32 .= Rotate (f,p) by FINSEQ_1:34 ; ::_thesis: verum end; suppose not p in rng f ; ::_thesis: Rotate ((Rotate (f,p)),p) = Rotate (f,p) hence Rotate ((Rotate (f,p)),p) = Rotate (f,p) by Def2; ::_thesis: verum end; end; end; theorem :: FINSEQ_6:94 for D being non empty set for p being Element of D holds Rotate (<*p*>,p) = <*p*> proof let D be non empty set ; ::_thesis: for p being Element of D holds Rotate (<*p*>,p) = <*p*> let p be Element of D; ::_thesis: Rotate (<*p*>,p) = <*p*> <*p*> /. 1 = p by FINSEQ_4:16; hence Rotate (<*p*>,p) = <*p*> by Th89; ::_thesis: verum end; theorem Th95: :: FINSEQ_6:95 for D being non empty set for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p1) = <*p1,p2*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p1) = <*p1,p2*> let p1, p2 be Element of D; ::_thesis: Rotate (<*p1,p2*>,p1) = <*p1,p2*> <*p1,p2*> /. 1 = p1 by FINSEQ_4:17; hence Rotate (<*p1,p2*>,p1) = <*p1,p2*> by Th89; ::_thesis: verum end; theorem :: FINSEQ_6:96 for D being non empty set for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p2) = <*p2,p2*> proof let D be non empty set ; ::_thesis: for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p2) = <*p2,p2*> let p1, p2 be Element of D; ::_thesis: Rotate (<*p1,p2*>,p2) = <*p2,p2*> percases ( p1 = p2 or p1 <> p2 ) ; suppose p1 = p2 ; ::_thesis: Rotate (<*p1,p2*>,p2) = <*p2,p2*> hence Rotate (<*p1,p2*>,p2) = <*p2,p2*> by Th95; ::_thesis: verum end; supposeA1: p1 <> p2 ; ::_thesis: Rotate (<*p1,p2*>,p2) = <*p2,p2*> rng <*p1,p2*> = {p1,p2} by Lm1; then p2 in rng <*p1,p2*> by TARSKI:def_2; hence Rotate (<*p1,p2*>,p2) = (<*p1,p2*> :- p2) ^ ((<*p1,p2*> -: p2) /^ 1) by Def2 .= <*p2*> ^ ((<*p1,p2*> -: p2) /^ 1) by A1, Th53 .= <*p2*> ^ (<*p1,p2*> /^ 1) by A1, Th49 .= <*p2*> ^ <*p2*> by Th46 .= <*p2,p2*> by FINSEQ_1:def_9 ; ::_thesis: verum end; end; end; theorem Th97: :: FINSEQ_6:97 for D being non empty set for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*> let p1, p2, p3 be Element of D; ::_thesis: Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*> <*p1,p2,p3*> /. 1 = p1 by FINSEQ_4:18; hence Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*> by Th89; ::_thesis: verum end; theorem :: FINSEQ_6:98 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> proof let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D st p1 <> p2 holds Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> let p1, p2, p3 be Element of D; ::_thesis: ( p1 <> p2 implies Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> ) assume A1: p1 <> p2 ; ::_thesis: Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> rng <*p1,p2,p3*> = {p1,p2,p3} by Lm2; then p2 in rng <*p1,p2,p3*> by ENUMSET1:def_1; hence Rotate (<*p1,p2,p3*>,p2) = (<*p1,p2,p3*> :- p2) ^ ((<*p1,p2,p3*> -: p2) /^ 1) by Def2 .= <*p2,p3*> ^ ((<*p1,p2,p3*> -: p2) /^ 1) by A1, Th54 .= <*p2,p3*> ^ (<*p1,p2*> /^ 1) by A1, Th50 .= <*p2,p3*> ^ <*p2*> by Th46 .= <*p2,p3,p2*> by FINSEQ_1:43 ; ::_thesis: verum end; theorem :: FINSEQ_6:99 for D being non empty set for p2, p3, p1 being Element of D st p2 <> p3 holds Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> proof let D be non empty set ; ::_thesis: for p2, p3, p1 being Element of D st p2 <> p3 holds Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> let p2, p3, p1 be Element of D; ::_thesis: ( p2 <> p3 implies Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> ) assume A1: p2 <> p3 ; ::_thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> percases ( p1 = p3 or p1 <> p3 ) ; suppose p1 = p3 ; ::_thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> hence Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> by Th97; ::_thesis: verum end; supposeA2: p1 <> p3 ; ::_thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> rng <*p1,p2,p3*> = {p1,p2,p3} by Lm2; then p3 in rng <*p1,p2,p3*> by ENUMSET1:def_1; hence Rotate (<*p1,p2,p3*>,p3) = (<*p1,p2,p3*> :- p3) ^ ((<*p1,p2,p3*> -: p3) /^ 1) by Def2 .= <*p3*> ^ ((<*p1,p2,p3*> -: p3) /^ 1) by A1, A2, Th55 .= <*p3*> ^ (<*p1,p2,p3*> /^ 1) by A1, A2, Th51 .= <*p3*> ^ <*p2,p3*> by Th47 .= <*p3,p2,p3*> by FINSEQ_1:43 ; ::_thesis: verum end; end; end; theorem :: FINSEQ_6:100 for D being non empty set for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f proof let D be non empty set ; ::_thesis: for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f let f be non trivial circular FinSequence of D; ::_thesis: rng (f /^ 1) = rng f thus rng (f /^ 1) c= rng f by FINSEQ_5:33; :: according to XBOOLE_0:def_10 ::_thesis: rng f c= rng (f /^ 1) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in rng (f /^ 1) ) f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29; then A1: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31; assume A2: x in rng f ; ::_thesis: x in rng (f /^ 1) percases ( x in rng <*(f /. 1)*> or x in rng (f /^ 1) ) by A1, A2, XBOOLE_0:def_3; suppose x in rng <*(f /. 1)*> ; ::_thesis: x in rng (f /^ 1) then x in {(f /. 1)} by FINSEQ_1:39; then x = f /. 1 by TARSKI:def_1; then A3: x = f /. (len f) by Def1; A4: len f >= 1 + 1 by NAT_D:60; then len f >= 1 by XXREAL_0:2; then A5: len (f /^ 1) = (len f) - 1 by RFINSEQ:def_1; then 1 <= len (f /^ 1) by A4, XREAL_1:19; then A6: len (f /^ 1) in dom (f /^ 1) by FINSEQ_3:25; (len (f /^ 1)) + 1 = len f by A5; then x = (f /^ 1) /. (len (f /^ 1)) by A3, A6, FINSEQ_5:27; hence x in rng (f /^ 1) by A6, PARTFUN2:2; ::_thesis: verum end; suppose x in rng (f /^ 1) ; ::_thesis: x in rng (f /^ 1) hence x in rng (f /^ 1) ; ::_thesis: verum end; end; end; theorem Th101: :: FINSEQ_6:101 for D being non empty set for p being Element of D for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p)) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p)) let p be Element of D; ::_thesis: for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p)) let f be FinSequence of D; ::_thesis: rng (f /^ 1) c= rng (Rotate (f,p)) percases ( p in rng f or not p in rng f ) ; supposeA1: p in rng f ; ::_thesis: rng (f /^ 1) c= rng (Rotate (f,p)) then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2; then A2: rng (Rotate (f,p)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31; thus rng (f /^ 1) c= rng (Rotate (f,p)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f /^ 1) or x in rng (Rotate (f,p)) ) assume A3: x in rng (f /^ 1) ; ::_thesis: x in rng (Rotate (f,p)) A4: rng (f /^ 1) c= rng f by FINSEQ_5:33; then A5: x in rng f by A3; percases ( ( x .. f < p .. f & x .. (f /^ 1) >= p .. (f /^ 1) ) or ( x .. f < p .. f & x .. (f /^ 1) <= p .. (f /^ 1) ) or x .. f >= p .. f ) ; supposethat A6: x .. f < p .. f and A7: x .. (f /^ 1) >= p .. (f /^ 1) ; ::_thesis: x in rng (Rotate (f,p)) A8: p .. f >= 1 by A1, FINSEQ_4:21; p .. f <> 1 by A3, A4, A6, FINSEQ_4:21; then p .. f > 1 by A8, XXREAL_0:1; then p .. f = (p .. (f /^ 1)) + 1 by A1, Th56; then A9: (x .. (f /^ 1)) + 1 >= p .. f by A7, XREAL_1:6; rng f c= D by FINSEQ_1:def_4; then reconsider q = x as Element of D by A5; A10: x .. (f /^ 1) in dom (f /^ 1) by A3, FINSEQ_4:20; f <> {} by A1; then len f >= 1 by NAT_1:14; then (len f) - 1 = len (f /^ 1) by RFINSEQ:def_1; then A11: len f = (len (f /^ 1)) + 1 ; x .. (f /^ 1) <= len (f /^ 1) by A3, FINSEQ_4:21; then A12: (x .. (f /^ 1)) + 1 <= len f by A11, XREAL_1:6; q = (f /^ 1) /. (q .. (f /^ 1)) by A3, FINSEQ_5:38 .= f /. ((q .. (f /^ 1)) + 1) by A10, FINSEQ_5:27 ; then x in rng (f :- p) by A1, A12, A9, Th63; hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; supposethat A13: x .. f < p .. f and A14: x .. (f /^ 1) <= p .. (f /^ 1) ; ::_thesis: x in rng (Rotate (f,p)) A15: p .. f <> 1 by A3, A4, A13, FINSEQ_4:21; p .. f >= 1 by A1, FINSEQ_4:21; then p .. f > 1 by A15, XXREAL_0:1; then p in rng (f /^ 1) by A1, Th57; then x in rng ((f /^ 1) -: p) by A3, A14, FINSEQ_5:46; then x in rng ((f -: p) /^ 1) by A1, A15, Th60; hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; suppose x .. f >= p .. f ; ::_thesis: x in rng (Rotate (f,p)) then x in rng (f :- p) by A1, A3, A4, Th62; hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; suppose not p in rng f ; ::_thesis: rng (f /^ 1) c= rng (Rotate (f,p)) then Rotate (f,p) = f by Def2; hence rng (f /^ 1) c= rng (Rotate (f,p)) by FINSEQ_5:33; ::_thesis: verum end; end; end; theorem Th102: :: FINSEQ_6:102 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proof let D be non empty set ; ::_thesis: for p2, p1 being Element of D for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let p2, p1 be Element of D; ::_thesis: for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let f be FinSequence of D; ::_thesis: ( p2 in (rng f) \ (rng (f -: p1)) implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) assume A1: p2 in (rng f) \ (rng (f -: p1)) ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) percases ( p1 in rng f or not p1 in rng f ) ; supposeA2: p1 in rng f ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) then A3: Rotate (f,p1) = (f :- p1) ^ ((f -: p1) /^ 1) by Def2; A4: p1 .. (f :- p1) = 1 by Th79; rng ((f -: p1) /^ 1) c= rng (f -: p1) by FINSEQ_5:33; then A5: not p2 in rng ((f -: p1) /^ 1) by A1, XBOOLE_0:def_5; A6: rng (f /^ 1) c= rng (Rotate (f,p1)) by Th101; A7: f -: p1 <> {} by A2, FINSEQ_5:47; A8: not p2 in rng (f -: p1) by A1, XBOOLE_0:def_5; p1 .. f <= p1 .. f ; then A9: p1 <> p2 by A2, A8, FINSEQ_5:46; rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A2, Th70; then A10: p2 in rng (f :- p1) by A1, A8, XBOOLE_0:def_3; p1 in rng (f :- p1) by Th61; then A11: p2 .. (f :- p1) <> 1 by A10, A9, A4, FINSEQ_5:9; then p2 in rng ((f :- p1) /^ 1) by A10, Th78; then A12: p2 in (rng ((f :- p1) /^ 1)) \ (rng ((f -: p1) /^ 1)) by A5, XBOOLE_0:def_5; A13: now__::_thesis:_not_p2_.._f_=_1 assume p2 .. f = 1 ; ::_thesis: contradiction then p2 .. f <= p1 .. f by A2, FINSEQ_4:21; hence contradiction by A1, A2, A8, FINSEQ_5:46; ::_thesis: verum end; then p2 in rng (f /^ 1) by A1, Th78; hence Rotate ((Rotate (f,p1)),p2) = (((f :- p1) ^ ((f -: p1) /^ 1)) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A3, A6, Def2 .= (((f :- p1) :- p2) ^ ((f -: p1) /^ 1)) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A10, Th64 .= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A1, A2, Th71 .= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) -: p2) /^ 1) by A10, Th66 .= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) /^ 1) -: p2) by A10, A11, Th60 .= (f :- p2) ^ (((f -: p1) /^ 1) ^ (((f :- p1) /^ 1) -: p2)) by FINSEQ_1:32 .= (f :- p2) ^ ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) -: p2) by A12, Th67 .= (f :- p2) ^ ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) -: p2) by A7, Th77 .= (f :- p2) ^ ((f /^ 1) -: p2) by A2, Th76 .= (f :- p2) ^ ((f -: p2) /^ 1) by A1, A13, Th60 .= Rotate (f,p2) by A1, Def2 ; ::_thesis: verum end; suppose not p1 in rng f ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Def2; ::_thesis: verum end; end; end; theorem Th103: :: FINSEQ_6:103 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proof let D be non empty set ; ::_thesis: for p2, p1 being Element of D for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let p2, p1 be Element of D; ::_thesis: for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let f be FinSequence of D; ::_thesis: ( p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) assume that A1: p2 .. f <> 1 and A2: p2 in (rng f) \ (rng (f :- p1)) ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) percases ( p1 in rng f or not p1 in rng f ) ; supposeA3: p1 in rng f ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) then A4: f -: p1 <> {} by FINSEQ_5:47; A5: not p2 in rng (f :- p1) by A2, XBOOLE_0:def_5; rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A3, Th70; then A6: p2 in rng (f -: p1) by A2, A5, XBOOLE_0:def_3; (f -: p1) ^ ((f :- p1) /^ 1) = f by A3, Th76; then A7: p2 .. (f -: p1) <> 1 by A1, A6, Th6; then A8: p2 in rng ((f -: p1) /^ 1) by A6, Th78; then A9: p2 in (rng ((f -: p1) /^ 1)) \ (rng (f :- p1)) by A5, XBOOLE_0:def_5; A10: Rotate (f,p1) = (f :- p1) ^ ((f -: p1) /^ 1) by A3, Def2; then rng (Rotate (f,p1)) = (rng (f :- p1)) \/ (rng ((f -: p1) /^ 1)) by FINSEQ_1:31; then p2 in rng (Rotate (f,p1)) by A8, XBOOLE_0:def_3; hence Rotate ((Rotate (f,p1)),p2) = (((f :- p1) ^ ((f -: p1) /^ 1)) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A10, Def2 .= (((f -: p1) /^ 1) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A9, Th65 .= (((f -: p1) /^ 1) :- p2) ^ (((f :- p1) ^ (((f -: p1) /^ 1) -: p2)) /^ 1) by A9, Th67 .= (((f -: p1) /^ 1) :- p2) ^ (((f :- p1) /^ 1) ^ (((f -: p1) /^ 1) -: p2)) by Th77 .= ((((f -: p1) /^ 1) :- p2) ^ ((f :- p1) /^ 1)) ^ (((f -: p1) /^ 1) -: p2) by FINSEQ_1:32 .= ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) :- p2) ^ (((f -: p1) /^ 1) -: p2) by A8, Th64 .= ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2) by A4, Th77 .= ((f /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2) by A3, Th76 .= (f :- p2) ^ (((f -: p1) /^ 1) -: p2) by A1, A2, Th83 .= (f :- p2) ^ (((f -: p1) -: p2) /^ 1) by A6, A7, Th60 .= (f :- p2) ^ ((f -: p2) /^ 1) by A3, A6, Th75 .= Rotate (f,p2) by A2, Def2 ; ::_thesis: verum end; suppose not p1 in rng f ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Def2; ::_thesis: verum end; end; end; theorem Th104: :: FINSEQ_6:104 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proof let D be non empty set ; ::_thesis: for p2, p1 being Element of D for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let p2, p1 be Element of D; ::_thesis: for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let f be FinSequence of D; ::_thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) percases ( p1 in rng f or not p1 in rng f ) ; supposeA1: p1 in rng f ; ::_thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) assume that A2: p2 in rng (f /^ 1) and A3: f just_once_values p2 ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:51; then A4: p2 in (rng ((f -| p1) ^ <*p1*>)) \+\ (rng (f |-- p1)) by A3, Th16; A5: now__::_thesis:_(_(_p2_in_rng_((f_-|_p1)_^_<*p1*>)_&_not_p2_in_rng_(f_|--_p1)_&_(_p2_in_rng_(f_:-_p1)_implies_p1_=_p2_)_)_or_(_not_p2_in_rng_((f_-|_p1)_^_<*p1*>)_&_not_p2_in_rng_(f_-:_p1)_)_) percases ( ( p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f |-- p1) ) or not p2 in rng ((f -| p1) ^ <*p1*>) ) by A4, XBOOLE_0:1; casethat p2 in rng ((f -| p1) ^ <*p1*>) and A6: not p2 in rng (f |-- p1) ; ::_thesis: ( p2 in rng (f :- p1) implies p1 = p2 ) now__::_thesis:_(_(_not_p2_in_rng_<*p1*>_&_not_p2_in_rng_(f_:-_p1)_)_or_(_p2_in_rng_<*p1*>_&_p2_=_p1_)_) percases ( not p2 in rng <*p1*> or p2 in rng <*p1*> ) ; case not p2 in rng <*p1*> ; ::_thesis: not p2 in rng (f :- p1) then not p2 in (rng (f |-- p1)) \/ (rng <*p1*>) by A6, XBOOLE_0:def_3; then not p2 in rng (<*p1*> ^ (f |-- p1)) by FINSEQ_1:31; hence not p2 in rng (f :- p1) by A1, Th41; ::_thesis: verum end; case p2 in rng <*p1*> ; ::_thesis: p2 = p1 then p2 in {p1} by FINSEQ_1:39; hence p2 = p1 by TARSKI:def_1; ::_thesis: verum end; end; end; hence ( p2 in rng (f :- p1) implies p1 = p2 ) ; ::_thesis: verum end; case not p2 in rng ((f -| p1) ^ <*p1*>) ; ::_thesis: not p2 in rng (f -: p1) hence not p2 in rng (f -: p1) by A1, Th40; ::_thesis: verum end; end; end; A7: p2 in rng f by A3, FINSEQ_4:5; then f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29, RELAT_1:38; then p2 in (rng <*(f /. 1)*>) \+\ (rng (f /^ 1)) by A3, Th16; then not p2 in rng <*(f /. 1)*> by A2, XBOOLE_0:1; then not p2 in {(f /. 1)} by FINSEQ_1:39; then p2 <> f /. 1 by TARSKI:def_1; then A8: p2 .. f <> 1 by A7, FINSEQ_5:38; now__::_thesis:_Rotate_((Rotate_(f,p1)),p2)_=_Rotate_(f,p2) percases ( p1 = p2 or p2 in (rng f) \ (rng (f -: p1)) or p2 in (rng f) \ (rng (f :- p1)) ) by A7, A5, XBOOLE_0:def_5; suppose p1 = p2 ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; ::_thesis: verum end; suppose p2 in (rng f) \ (rng (f -: p1)) ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th102; ::_thesis: verum end; suppose p2 in (rng f) \ (rng (f :- p1)) ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by A8, Th103; ::_thesis: verum end; end; end; hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ; ::_thesis: verum end; suppose not p1 in rng f ; ::_thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) hence ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) by Def2; ::_thesis: verum end; end; end; theorem :: FINSEQ_6:105 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st f is circular & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proof let D be non empty set ; ::_thesis: for p2, p1 being Element of D for f being FinSequence of D st f is circular & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let p2, p1 be Element of D; ::_thesis: for f being FinSequence of D st f is circular & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) let f be FinSequence of D; ::_thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) percases ( p1 in rng f or not p1 in rng f ) ; supposeA1: p1 in rng f ; ::_thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) assume that A2: f is circular and A3: f just_once_values p2 ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) A4: p2 in rng f by A3, FINSEQ_4:45; now__::_thesis:_Rotate_((Rotate_(f,p1)),p2)_=_Rotate_(f,p2) percases ( rng f is trivial or not rng f is trivial ) ; suppose rng f is trivial ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) then p1 = p2 by A1, A4, ZFMISC_1:def_10; hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; ::_thesis: verum end; supposeA5: not rng f is trivial ; ::_thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) then f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29, RELAT_1:38; then A6: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31; now__::_thesis:_p2_in_rng_(f_/^_1) not f is trivial by A5; then len f >= 1 + 1 by NAT_D:60; then A7: 1 < len f by NAT_1:13; assume A8: not p2 in rng (f /^ 1) ; ::_thesis: contradiction then p2 in rng <*(f /. 1)*> by A4, A6, XBOOLE_0:def_3; then p2 in {(f /. 1)} by FINSEQ_1:39; then p2 = f /. 1 by TARSKI:def_1; then A9: p2 = f /. (len f) by A2, Def1; len f in dom f by A5, FINSEQ_5:6, RELAT_1:38; hence contradiction by A8, A9, A7, Th58; ::_thesis: verum end; hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by A3, Th104; ::_thesis: verum end; end; end; hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ; ::_thesis: verum end; suppose not p1 in rng f ; ::_thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) hence ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) by Def2; ::_thesis: verum end; end; end; theorem :: FINSEQ_6:106 for D being non empty set for p being Element of D for f being FinSequence of D st f is circular & f just_once_values p holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st f is circular & f just_once_values p holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) let p be Element of D; ::_thesis: for f being FinSequence of D st f is circular & f just_once_values p holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) let f be FinSequence of D; ::_thesis: ( f is circular & f just_once_values p implies Rev (Rotate (f,p)) = Rotate ((Rev f),p) ) assume that A1: f is circular and A2: f just_once_values p ; ::_thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p) reconsider j = (len (f :- p)) - 1 as Element of NAT by INT_1:5, NAT_1:14; A3: f /. 1 = f /. (len f) by A1, Def1; A4: p in rng f by A2, FINSEQ_4:45; then A5: f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by FINSEQ_5:29, FINSEQ_5:47 .= <*(f /. 1)*> ^ ((f -: p) /^ 1) by A4, FINSEQ_5:44 ; A6: j + 1 = len (f :- p) ; then A7: f :- p = ((f :- p) | j) ^ <*((f :- p) /. (len (f :- p)))*> by FINSEQ_5:21 .= ((f :- p) | j) ^ <*(f /. (len f))*> by A4, FINSEQ_5:54 ; A8: p in rng (Rev f) by A4, FINSEQ_5:57; thus Rev (Rotate (f,p)) = Rev ((f :- p) ^ ((f -: p) /^ 1)) by A4, Def2 .= (Rev ((f -: p) /^ 1)) ^ (Rev (f :- p)) by FINSEQ_5:64 .= (Rev ((f -: p) /^ 1)) ^ (<*(f /. (len f))*> ^ (Rev ((f :- p) | j))) by A7, FINSEQ_5:63 .= ((Rev ((f -: p) /^ 1)) ^ <*(f /. 1)*>) ^ (Rev ((f :- p) | j)) by A3, FINSEQ_1:32 .= (Rev (f -: p)) ^ (Rev ((f :- p) | j)) by A5, Th24 .= (Rev (f -: p)) ^ ((Rev (f :- p)) /^ 1) by A6, Th85 .= (Rev (f -: p)) ^ (((Rev f) -: p) /^ 1) by A2, Th87 .= ((Rev f) :- p) ^ (((Rev f) -: p) /^ 1) by A2, Th88 .= Rotate ((Rev f),p) by A8, Def2 ; ::_thesis: verum end; begin theorem :: FINSEQ_6:107 for D being non empty set for f being trivial FinSequence of D holds ( f is empty or ex x being Element of D st f = <*x*> ) proof let D be non empty set ; ::_thesis: for f being trivial FinSequence of D holds ( f is empty or ex x being Element of D st f = <*x*> ) let f be trivial FinSequence of D; ::_thesis: ( f is empty or ex x being Element of D st f = <*x*> ) A1: rng f c= D by FINSEQ_1:def_4; assume not f is empty ; ::_thesis: ex x being Element of D st f = <*x*> then consider x being set such that A2: f = {x} by ZFMISC_1:131; A3: 1 in dom f by A2, FINSEQ_5:6; A4: x in {x} by TARSKI:def_1; then consider y, z being set such that A5: x = [y,z] by A2, RELAT_1:def_1; take z ; ::_thesis: ( z is Element of D & f = <*z*> ) z in rng f by A2, A4, A5, XTUPLE_0:def_13; hence z is Element of D by A1; ::_thesis: f = <*z*> dom f = {y} by A2, A5, RELAT_1:9; then 1 = y by A3, TARSKI:def_1; hence f = <*z*> by A2, A5, FINSEQ_1:def_5; ::_thesis: verum end; begin theorem :: FINSEQ_6:108 for i being Nat for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds (p ^ q) . i = q . (i - (len p)) proof let i be Nat; ::_thesis: for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds (p ^ q) . i = q . (i - (len p)) let p, q be FinSequence; ::_thesis: ( len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) implies (p ^ q) . i = q . (i - (len p)) ) assume that A1: len p < i and A2: ( i <= (len p) + (len q) or i <= len (p ^ q) ) ; ::_thesis: (p ^ q) . i = q . (i - (len p)) i <= (len p) + (len q) by A2, FINSEQ_1:22; then A3: i - (len p) <= ((len p) + (len q)) - (len p) by XREAL_1:9; (len p) + 1 <= i by A1, NAT_1:13; then A4: ((len p) + 1) - (len p) <= i - (len p) by XREAL_1:9; then A5: (len p) + (i -' (len p)) = (len p) + (i - (len p)) by XREAL_0:def_2 .= i ; i - (len p) = i -' (len p) by A4, XREAL_0:def_2; then i -' (len p) in dom q by A4, A3, FINSEQ_3:25; hence (p ^ q) . i = q . (i - (len p)) by A5, FINSEQ_1:def_7; ::_thesis: verum end; theorem :: FINSEQ_6:109 for D being non empty set for x being set for f being FinSequence of D st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) proof let D be non empty set ; ::_thesis: for x being set for f being FinSequence of D st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) let x be set ; ::_thesis: for f being FinSequence of D st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) let f be FinSequence of D; ::_thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) ) assume A1: 1 <= len f ; ::_thesis: ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) then A2: len f in dom f by FINSEQ_3:25; 1 in dom f by A1, FINSEQ_3:25; then A3: (f ^ <*x*>) . 1 = f . 1 by FINSEQ_1:def_7; (<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39 .= f . (len f) by A2, FINSEQ_1:def_7 ; hence ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) by A1, A3, FINSEQ_4:15; ::_thesis: verum end; theorem Th110: :: FINSEQ_6:110 for f being FinSequence st len f = 1 holds Rev f = f proof let f be FinSequence; ::_thesis: ( len f = 1 implies Rev f = f ) assume len f = 1 ; ::_thesis: Rev f = f then f = <*(f . 1)*> by FINSEQ_1:40; hence Rev f = f by FINSEQ_5:60; ::_thesis: verum end; theorem :: FINSEQ_6:111 for D being non empty set for f being FinSequence of D for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29; theorem :: FINSEQ_6:112 for D being non empty set for f being FinSequence of D for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by FINSEQ_5:80; definition let f be FinSequence; let k1, k2 be Nat; func mid (f,k1,k2) -> FinSequence equals :Def3: :: FINSEQ_6:def 3 (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2 otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)); correctness coherence ( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence ) ); consistency for b1 being FinSequence holds verum; ; end; :: deftheorem Def3 defines mid FINSEQ_6:def_3_:_ for f being FinSequence for k1, k2 being Nat holds ( ( k1 <= k2 implies mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) ); definition let D be non empty set ; let f be FinSequence of D; let k1, k2 be Nat; :: original: mid redefine func mid (f,k1,k2) -> FinSequence of D; coherence mid (f,k1,k2) is FinSequence of D proof ( mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) or mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) by Def3; hence mid (f,k1,k2) is FinSequence of D ; ::_thesis: verum end; end; theorem :: FINSEQ_6:113 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) let k1, k2 be Element of NAT ; ::_thesis: ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f implies Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ) assume that A1: 1 <= k1 and A2: k1 <= len f and A3: 1 <= k2 and A4: k2 <= len f ; ::_thesis: Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) percases ( k1 <= k2 or k1 > k2 ) ; supposeA5: k1 <= k2 ; ::_thesis: Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) A6: (len f) -' (k1 -' 1) = (len f) - (k1 -' 1) by A2, NAT_D:50, XREAL_1:233 .= (len f) - (k1 - 1) by A1, XREAL_1:233 .= ((len f) - k1) + 1 .= ((len f) -' k1) + 1 by A2, XREAL_1:233 ; A7: (len f) -' k1 = (len f) - k1 by A2, XREAL_1:233; A8: (len f) -' k2 = (len f) - k2 by A4, XREAL_1:233; k2 - k1 <= (len f) - k1 by A4, XREAL_1:9; then k2 -' k1 <= (len f) - k1 by A5, XREAL_1:233; then k2 -' k1 <= (len f) -' k1 by A2, XREAL_1:233; then (k2 -' k1) + 1 <= ((len f) -' k1) + 1 by XREAL_1:6; then A9: ((len f) -' (k1 -' 1)) -' ((k2 -' k1) + 1) = (((len f) -' k1) + 1) - ((k2 -' k1) + 1) by A6, XREAL_1:233 .= (((len f) - k1) + 1) - ((k2 - k1) + 1) by A5, A7, XREAL_1:233 .= (((len f) + 1) - 1) - k2 .= (len f) -' k2 by A4, XREAL_1:233 ; then A10: ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) + ((k2 -' k1) + 1) = ((len f) -' k2) + ((k2 -' k1) + 1) by RFINSEQ:29 .= ((len f) - k2) + ((k2 - k1) + 1) by A5, A8, XREAL_1:233 .= (len f) - (k1 - 1) .= (len f) - (k1 -' 1) by A1, XREAL_1:233 .= (len f) -' (k1 -' 1) by A2, NAT_D:50, XREAL_1:233 .= len (f /^ (k1 -' 1)) by RFINSEQ:29 ; A11: (len f) -' k1 <= ((len f) -' k1) + 1 by NAT_1:11; (len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41; then A12: ((len f) -' (k1 -' 1)) -' ((len f) -' k2) = (((len f) -' k1) + 1) - ((len f) -' k2) by A6, A11, XREAL_1:233, XXREAL_0:2 .= (((len f) - k1) + 1) - ((len f) - k2) by A4, A7, XREAL_1:233 .= (k2 - k1) + 1 .= (k2 -' k1) + 1 by A5, XREAL_1:233 ; A13: ((len f) -' (k1 -' 1)) + (k1 -' 1) = ((len f) - (k1 -' 1)) + (k1 -' 1) by A2, NAT_D:50, XREAL_1:233 .= len f ; (len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41; then ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:6; then A14: ((((len f) -' k1) + 1) -' (((len f) -' k2) + 1)) + 1 = ((((len f) -' k1) + 1) - (((len f) -' k2) + 1)) + 1 by XREAL_1:233 .= ((((len f) - k1) + 1) - (((len f) - k2) + 1)) + 1 by A4, A7, XREAL_1:233 .= (k2 - k1) + 1 .= (k2 -' k1) + 1 by A5, XREAL_1:233 ; (len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41; then ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:6; then mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) = ((Rev f) /^ ((((len f) -' k2) + 1) -' 1)) | ((k2 -' k1) + 1) by A14, Def3 .= ((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2)) by A12, NAT_D:34 .= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len f) -' k2) by FINSEQ_5:80 .= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A9, RFINSEQ:29 .= (Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A13, Th84 .= Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) by A10, Th85 .= Rev (mid (f,k1,k2)) by A5, Def3 ; hence Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ; ::_thesis: verum end; supposeA15: k1 > k2 ; ::_thesis: Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) A16: (len f) -' (k2 -' 1) = (len f) - (k2 -' 1) by A4, NAT_D:50, XREAL_1:233 .= (len f) - (k2 - 1) by A3, XREAL_1:233 .= ((len f) - k2) + 1 .= ((len f) -' k2) + 1 by A4, XREAL_1:233 ; A17: (len f) -' k2 = (len f) - k2 by A4, XREAL_1:233; (len f) -' k2 >= (len f) -' k1 by A15, NAT_D:41; then ((len f) -' k2) + 1 >= ((len f) -' k1) + 1 by XREAL_1:6; then A18: ((((len f) -' k2) + 1) -' (((len f) -' k1) + 1)) + 1 = ((((len f) -' k2) + 1) - (((len f) -' k1) + 1)) + 1 by XREAL_1:233 .= ((((len f) - k2) + 1) - (((len f) - k1) + 1)) + 1 by A2, A17, XREAL_1:233 .= (k1 - k2) + 1 .= (k1 -' k2) + 1 by A15, XREAL_1:233 ; A19: (len f) -' k1 = (len f) - k1 by A2, XREAL_1:233; A20: (len f) -' k2 <= ((len f) -' k2) + 1 by NAT_1:11; (len f) -' k2 >= (len f) -' k1 by A15, NAT_D:41; then A21: ((len f) -' (k2 -' 1)) -' ((len f) -' k1) = (((len f) -' k2) + 1) - ((len f) -' k1) by A16, A20, XREAL_1:233, XXREAL_0:2 .= (((len f) - k2) + 1) - ((len f) - k1) by A2, A17, XREAL_1:233 .= (k1 - k2) + 1 .= (k1 -' k2) + 1 by A15, XREAL_1:233 ; A22: ((len f) -' (k2 -' 1)) + (k2 -' 1) = ((len f) - (k2 -' 1)) + (k2 -' 1) by A4, NAT_D:50, XREAL_1:233 .= len f ; k1 - k2 <= (len f) - k2 by A2, XREAL_1:9; then k1 -' k2 <= (len f) - k2 by A15, XREAL_1:233; then k1 -' k2 <= (len f) -' k2 by A4, XREAL_1:233; then (k1 -' k2) + 1 <= ((len f) -' k2) + 1 by XREAL_1:6; then A23: ((len f) -' (k2 -' 1)) -' ((k1 -' k2) + 1) = (((len f) -' k2) + 1) - ((k1 -' k2) + 1) by A16, XREAL_1:233 .= (((len f) - k2) + 1) - ((k1 - k2) + 1) by A15, A17, XREAL_1:233 .= (((len f) + 1) - 1) - k1 .= (len f) -' k1 by A2, XREAL_1:233 ; then A24: ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) + ((k1 -' k2) + 1) = ((len f) -' k1) + ((k1 -' k2) + 1) by RFINSEQ:29 .= ((len f) - k1) + ((k1 - k2) + 1) by A15, A19, XREAL_1:233 .= (len f) - (k2 - 1) .= (len f) - (k2 -' 1) by A3, XREAL_1:233 .= (len f) -' (k2 -' 1) by A4, NAT_D:50, XREAL_1:233 .= len (f /^ (k2 -' 1)) by RFINSEQ:29 ; (len f) - k2 > (len f) - k1 by A15, XREAL_1:10; then ((len f) -' k2) + 1 > ((len f) -' k1) + 1 by A17, A19, XREAL_1:6; then mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) = Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1)) by A18, Def3 .= Rev (((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1))) by A21, NAT_D:34 .= Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len f) -' k1)) by FINSEQ_5:80 .= Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A23, RFINSEQ:29 .= Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A22, Th84 .= Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) by A24, Th85 .= Rev (mid (f,k1,k2)) by A15, Def3 ; hence Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ; ::_thesis: verum end; end; end; theorem Th114: :: FINSEQ_6:114 for D being non empty set for n, m being Element of NAT for f being FinSequence of D st 1 <= m & m + n <= len f holds (f /^ n) . m = f . (m + n) proof let D be non empty set ; ::_thesis: for n, m being Element of NAT for f being FinSequence of D st 1 <= m & m + n <= len f holds (f /^ n) . m = f . (m + n) let n, m be Element of NAT ; ::_thesis: for f being FinSequence of D st 1 <= m & m + n <= len f holds (f /^ n) . m = f . (m + n) let f be FinSequence of D; ::_thesis: ( 1 <= m & m + n <= len f implies (f /^ n) . m = f . (m + n) ) assume that A1: 1 <= m and A2: m + n <= len f ; ::_thesis: (f /^ n) . m = f . (m + n) A3: (m + n) - n <= (len f) - n by A2, XREAL_1:9; n <= n + m by NAT_1:11; then A4: n <= len f by A2, XXREAL_0:2; then len (f /^ n) = (len f) - n by RFINSEQ:def_1; then m in dom (f /^ n) by A1, A3, FINSEQ_3:25; hence (f /^ n) . m = f . (m + n) by A4, RFINSEQ:def_1; ::_thesis: verum end; theorem Th115: :: FINSEQ_6:115 for D being non empty set for i being Element of NAT for f being FinSequence of D st 1 <= i & i <= len f holds (Rev f) . i = f . (((len f) - i) + 1) proof let D be non empty set ; ::_thesis: for i being Element of NAT for f being FinSequence of D st 1 <= i & i <= len f holds (Rev f) . i = f . (((len f) - i) + 1) let i be Element of NAT ; ::_thesis: for f being FinSequence of D st 1 <= i & i <= len f holds (Rev f) . i = f . (((len f) - i) + 1) let f be FinSequence of D; ::_thesis: ( 1 <= i & i <= len f implies (Rev f) . i = f . (((len f) - i) + 1) ) assume that A1: 1 <= i and A2: i <= len f ; ::_thesis: (Rev f) . i = f . (((len f) - i) + 1) i in dom f by A1, A2, FINSEQ_3:25; hence (Rev f) . i = f . (((len f) - i) + 1) by FINSEQ_5:58; ::_thesis: verum end; theorem :: FINSEQ_6:116 for D being non empty set for f being FinSequence of D for k being Nat st 1 <= k holds mid (f,1,k) = f | k proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k being Nat st 1 <= k holds mid (f,1,k) = f | k let f be FinSequence of D; ::_thesis: for k being Nat st 1 <= k holds mid (f,1,k) = f | k let k be Nat; ::_thesis: ( 1 <= k implies mid (f,1,k) = f | k ) 1 -' 1 = 0 by XREAL_1:232; then A1: f /^ (1 -' 1) = f by FINSEQ_5:28; assume A2: 1 <= k ; ::_thesis: mid (f,1,k) = f | k then mid (f,1,k) = (f /^ (1 -' 1)) | ((k -' 1) + 1) by Def3; hence mid (f,1,k) = f | k by A2, A1, XREAL_1:235; ::_thesis: verum end; theorem :: FINSEQ_6:117 for D being non empty set for f being FinSequence of D for k being Element of NAT st k <= len f holds mid (f,k,(len f)) = f /^ (k -' 1) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k being Element of NAT st k <= len f holds mid (f,k,(len f)) = f /^ (k -' 1) let f be FinSequence of D; ::_thesis: for k being Element of NAT st k <= len f holds mid (f,k,(len f)) = f /^ (k -' 1) let k be Element of NAT ; ::_thesis: ( k <= len f implies mid (f,k,(len f)) = f /^ (k -' 1) ) assume A1: k <= len f ; ::_thesis: mid (f,k,(len f)) = f /^ (k -' 1) then A2: mid (f,k,(len f)) = (f /^ (k -' 1)) | (((len f) -' k) + 1) by Def3; k -' 1 <= len f by A1, NAT_D:44; then A3: len (f /^ (k -' 1)) = (len f) - (k -' 1) by RFINSEQ:def_1; A4: ((len f) -' k) + 1 = ((len f) - k) + 1 by A1, XREAL_1:233 .= (len f) - (k - 1) ; now__::_thesis:_(_(_k_=_0_&_mid_(f,k,(len_f))_=_f_/^_(k_-'_1)_)_or_(_k_<>_0_&_mid_(f,k,(len_f))_=_f_/^_(k_-'_1)_)_) percases ( k = 0 or k <> 0 ) ; caseA5: k = 0 ; ::_thesis: mid (f,k,(len f)) = f /^ (k -' 1) 0 - 1 < 0 ; then k -' 1 = 0 by A5, XREAL_0:def_2; then A6: f /^ (k -' 1) = f by FINSEQ_5:28; ((len f) -' k) + 1 = (len f) + 1 by A5, NAT_D:40; then len f <= ((len f) -' k) + 1 by NAT_1:11; then Seg (len f) c= Seg (((len f) -' k) + 1) by FINSEQ_1:5; then dom (f /^ (k -' 1)) c= Seg (((len f) -' k) + 1) by A6, FINSEQ_1:def_3; then (f /^ (k -' 1)) | (Seg (((len f) -' k) + 1)) = f /^ (k -' 1) by RELAT_1:68; hence mid (f,k,(len f)) = f /^ (k -' 1) by A2, FINSEQ_1:def_15; ::_thesis: verum end; case k <> 0 ; ::_thesis: mid (f,k,(len f)) = f /^ (k -' 1) then 0 + 1 <= k by NAT_1:13; then len (f /^ (k -' 1)) = ((len f) -' k) + 1 by A3, A4, XREAL_1:233; hence mid (f,k,(len f)) = (f /^ (k -' 1)) | (Seg (len (f /^ (k -' 1)))) by A2, FINSEQ_1:def_15 .= (f /^ (k -' 1)) | (dom (f /^ (k -' 1))) by FINSEQ_1:def_3 .= f /^ (k -' 1) ; ::_thesis: verum end; end; end; hence mid (f,k,(len f)) = f /^ (k -' 1) ; ::_thesis: verum end; theorem Th118: :: FINSEQ_6:118 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds ( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds ( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) ) let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds ( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) ) let k11, k21 be Element of NAT ; ::_thesis: ( 1 <= k11 & k11 <= len f & 1 <= k21 & k21 <= len f implies ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) ) assume that A1: 1 <= k11 and A2: k11 <= len f and A3: 1 <= k21 and A4: k21 <= len f ; ::_thesis: ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) k21 -' 1 <= len f by A4, NAT_D:44; then A5: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def_1; A6: k21 - 1 >= 0 by A3, XREAL_1:48; then A7: k21 -' 1 = k21 - 1 by XREAL_0:def_2; A8: now__::_thesis:_for_k1,_k2_being_Element_of_NAT_st_k1_<=_k2_&_1_<=_k1_&_k1_<=_len_f_holds_ (mid_(f,k1,k2))_._1_=_f_._k1 let k1, k2 be Element of NAT ; ::_thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 ) now__::_thesis:_(_k1_<=_k2_&_1_<=_k1_&_k1_<=_len_f_implies_(mid_(f,k1,k2))_._1_=_f_._k1_) assume that A9: k1 <= k2 and A10: 1 <= k1 and A11: k1 <= len f ; ::_thesis: (mid (f,k1,k2)) . 1 = f . k1 A12: (mid (f,k1,k2)) . 1 = ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . 1 by A9, Def3 .= ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1 by FINSEQ_1:def_15 ; k1 - 1 >= 0 by A10, XREAL_1:48; then A13: 1 + (k1 -' 1) = 1 + (k1 - 1) by XREAL_0:def_2 .= k1 ; then 1 + (k1 -' 1) <= ((len f) - (k1 -' 1)) + (k1 -' 1) by A11; then A14: 1 <= (len f) - (k1 -' 1) by XREAL_1:6; A15: k1 -' 1 <= len f by A11, NAT_D:44; then len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by RFINSEQ:def_1; then 1 in Seg (len (f /^ (k1 -' 1))) by A14, FINSEQ_1:1; then A16: 1 in dom (f /^ (k1 -' 1)) by FINSEQ_1:def_3; 0 + 1 <= (k2 -' k1) + 1 by XREAL_1:6; then 1 in Seg ((k2 -' k1) + 1) by FINSEQ_1:1; then 1 in (dom (f /^ (k1 -' 1))) /\ (Seg ((k2 -' k1) + 1)) by A16, XBOOLE_0:def_4; then 1 in dom ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) by RELAT_1:61; then (mid (f,k1,k2)) . 1 = (f /^ (k1 -' 1)) . 1 by A12, FUNCT_1:47; hence (mid (f,k1,k2)) . 1 = f . k1 by A13, A15, A16, RFINSEQ:def_1; ::_thesis: verum end; hence ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 ) ; ::_thesis: verum end; thus (mid (f,k11,k21)) . 1 = f . k11 ::_thesis: ( ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) proof percases ( k11 <= k21 or k11 > k21 ) ; suppose k11 <= k21 ; ::_thesis: (mid (f,k11,k21)) . 1 = f . k11 hence (mid (f,k11,k21)) . 1 = f . k11 by A1, A2, A8; ::_thesis: verum end; supposeA17: k11 > k21 ; ::_thesis: (mid (f,k11,k21)) . 1 = f . k11 A18: k21 - 1 >= 0 by A3, XREAL_1:48; A19: k11 - k21 >= 0 by A17, XREAL_1:48; then k11 -' k21 = k11 - k21 by XREAL_0:def_2; then A20: (k21 -' 1) + ((k11 -' k21) + 1) = (k21 - 1) + (k11 - (k21 - 1)) by A18, XREAL_0:def_2 .= k11 ; k21 -' 1 <= len f by A4, NAT_D:44; then A21: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def_1; A22: 1 <= (k11 -' k21) + 1 by NAT_1:11; (k11 -' k21) + 1 = (k11 - k21) + 1 by A19, XREAL_0:def_2 .= k11 - (k21 - 1) .= k11 - (k21 -' 1) by A18, XREAL_0:def_2 ; then A23: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A21, XREAL_1:9; then A24: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by FINSEQ_1:59; then A25: (k11 -' k21) + 1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, FINSEQ_3:25; A26: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A22, A23, FINSEQ_3:25; A27: ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1) by A22, A24, FINSEQ_4:15 .= (f /^ (k21 -' 1)) /. ((k11 -' k21) + 1) by A25, FINSEQ_4:70 .= f /. ((k21 -' 1) + ((k11 -' k21) + 1)) by A26, FINSEQ_5:27 .= f . k11 by A1, A2, A20, FINSEQ_4:15 ; 1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, A24, FINSEQ_3:25; then (Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) . 1 = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - 1) + 1) by FINSEQ_5:58 .= f . k11 by A27 ; hence (mid (f,k11,k21)) . 1 = f . k11 by A17, Def3; ::_thesis: verum end; end; end; thus ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) ::_thesis: ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) proof A28: k11 - 1 >= 0 by A1, XREAL_1:48; then A29: k11 -' 1 = k11 - 1 by XREAL_0:def_2; k11 -' 1 <= len f by A2, NAT_D:44; then A30: len (f /^ (k11 -' 1)) = (len f) - (k11 -' 1) by RFINSEQ:def_1; assume A31: k11 <= k21 ; ::_thesis: ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) then A32: mid (f,k11,k21) = (f /^ (k11 -' 1)) | ((k21 -' k11) + 1) by Def3; A33: k21 - k11 >= 0 by A31, XREAL_1:48; then A34: k21 -' k11 = k21 - k11 by XREAL_0:def_2; (k21 -' k11) + 1 = (k21 - k11) + 1 by A33, XREAL_0:def_2 .= k21 - (k11 - 1) .= k21 - (k11 -' 1) by A28, XREAL_0:def_2 ; then A35: (k21 -' k11) + 1 <= len (f /^ (k11 -' 1)) by A4, A30, XREAL_1:9; then A36: len ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) = (k21 -' k11) + 1 by FINSEQ_1:59; for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) assume that A37: 1 <= i and A38: i <= len (mid (f,k11,k21)) ; ::_thesis: (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) A39: i <= (k21 -' k11) + 1 by A32, A35, A38, FINSEQ_1:59; i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1) by A32, A34, A36, A38, XREAL_1:6; then A40: i + (k11 -' 1) <= len f by A4, A29, XXREAL_0:2; A41: k11 <= k11 + i by NAT_1:11; A42: i + (k11 -' 1) = i + (k11 - 1) by A28, XREAL_0:def_2 .= (i + k11) - 1 .= (i + k11) -' 1 by A1, A41, XREAL_1:233, XXREAL_0:2 ; (mid (f,k11,k21)) . i = ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i by A31, Def3 .= (f /^ (k11 -' 1)) . i by A39, FINSEQ_3:112 .= f . (i + (k11 -' 1)) by A37, A40, Th114 ; hence (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) by A42; ::_thesis: verum end; hence ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) by A32, A35, FINSEQ_1:59; ::_thesis: verum end; assume A43: k11 > k21 ; ::_thesis: ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) then A44: k11 - k21 >= 0 by XREAL_1:48; then A45: k11 -' k21 = k11 - k21 by XREAL_0:def_2; A46: mid (f,k11,k21) = Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A43, Def3; then A47: len (mid (f,k11,k21)) = len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by FINSEQ_5:def_3; (k11 -' k21) + 1 = (k11 - k21) + 1 by A44, XREAL_0:def_2 .= k11 - (k21 - 1) .= k11 - (k21 -' 1) by A6, XREAL_0:def_2 ; then A48: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A5, XREAL_1:9; hence A49: len (mid (f,k11,k21)) = (k11 -' k21) + 1 by A47, FINSEQ_1:59; ::_thesis: for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) A50: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by A48, FINSEQ_1:59; thus for i being Element of NAT st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) assume that A51: 1 <= i and A52: i <= len (mid (f,k11,k21)) ; ::_thesis: (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) A53: i + (k21 - 1) <= (k11 - (k21 - 1)) + (k21 - 1) by A45, A49, A52, XREAL_1:6; (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i -' 1) by NAT_1:11; then (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i - 1) by A51, XREAL_1:233; then ((k11 -' k21) + 1) - (i - 1) <= (((k11 -' k21) + 1) + (i - 1)) - (i - 1) by XREAL_1:9; then A54: (((k11 -' k21) + 1) - i) + 1 <= (k11 -' k21) + 1 ; i <= (k11 -' k21) + 1 by A47, A48, A52, FINSEQ_1:59; then A55: (((k11 -' k21) + 1) -' i) + 1 <= (k11 -' k21) + 1 by A54, XREAL_1:233; A56: i + k11 <= i + (len f) by A2, XREAL_1:6; A57: i <= i + (k21 -' 1) by NAT_1:11; A58: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) = ((((k11 -' k21) + 1) - i) + 1) + (k21 -' 1) by A49, A52, XREAL_1:233 .= (((k11 - (k21 - 1)) - i) + 1) + (k21 - 1) by A6, A45, XREAL_0:def_2 .= (k11 - i) + 1 .= (k11 -' i) + 1 by A7, A53, A57, XREAL_1:233, XXREAL_0:2 ; 1 + k11 <= i + k11 by A51, XREAL_1:6; then 1 + k11 <= i + (len f) by A56, XXREAL_0:2; then (1 + k11) - i <= (i + (len f)) - i by XREAL_1:9; then (k11 - i) + 1 <= len f ; then A59: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) <= len f by A7, A53, A57, A58, XREAL_1:233, XXREAL_0:2; (mid (f,k11,k21)) . i = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1) by A46, A47, A51, A52, Th115 .= ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1) by A47, A52, XREAL_1:233 .= (f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1) by A50, A55, FINSEQ_3:112 .= f . ((k11 -' i) + 1) by A58, A59, Th114, NAT_1:11 ; hence (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ; ::_thesis: verum end; end; theorem :: FINSEQ_6:119 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT holds rng (mid (f,k1,k2)) c= rng f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT holds rng (mid (f,k1,k2)) c= rng f let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT holds rng (mid (f,k1,k2)) c= rng f let k1, k2 be Element of NAT ; ::_thesis: rng (mid (f,k1,k2)) c= rng f percases ( k1 <= k2 or k1 > k2 ) ; suppose k1 <= k2 ; ::_thesis: rng (mid (f,k1,k2)) c= rng f then mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) by Def3; then A1: rng (mid (f,k1,k2)) c= rng (f /^ (k1 -' 1)) by FINSEQ_5:19; rng (f /^ (k1 -' 1)) c= rng f by FINSEQ_5:33; hence rng (mid (f,k1,k2)) c= rng f by A1, XBOOLE_1:1; ::_thesis: verum end; suppose k1 > k2 ; ::_thesis: rng (mid (f,k1,k2)) c= rng f then mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by Def3; then rng (mid (f,k1,k2)) = rng ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by FINSEQ_5:57; then A2: rng (mid (f,k1,k2)) c= rng (f /^ (k2 -' 1)) by FINSEQ_5:19; rng (f /^ (k2 -' 1)) c= rng f by FINSEQ_5:33; hence rng (mid (f,k1,k2)) c= rng f by A2, XBOOLE_1:1; ::_thesis: verum end; end; end; theorem :: FINSEQ_6:120 for D being non empty set for f being FinSequence of D st 1 <= len f holds mid (f,1,(len f)) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D st 1 <= len f holds mid (f,1,(len f)) = f let f be FinSequence of D; ::_thesis: ( 1 <= len f implies mid (f,1,(len f)) = f ) assume A1: 1 <= len f ; ::_thesis: mid (f,1,(len f)) = f then mid (f,1,(len f)) = (f /^ (1 -' 1)) | (((len f) -' 1) + 1) by Def3 .= (f /^ 0) | (((len f) -' 1) + 1) by XREAL_1:232 .= f | (((len f) -' 1) + 1) by FINSEQ_5:28 .= f | (len f) by A1, XREAL_1:235 .= f by FINSEQ_1:58 ; hence mid (f,1,(len f)) = f ; ::_thesis: verum end; theorem :: FINSEQ_6:121 for D being non empty set for f being FinSequence of D st 1 <= len f holds mid (f,(len f),1) = Rev f proof let D be non empty set ; ::_thesis: for f being FinSequence of D st 1 <= len f holds mid (f,(len f),1) = Rev f let f be FinSequence of D; ::_thesis: ( 1 <= len f implies mid (f,(len f),1) = Rev f ) assume A1: 1 <= len f ; ::_thesis: mid (f,(len f),1) = Rev f A2: 1 -' 1 = 0 by XREAL_1:232; percases ( len f <> 1 or len f = 1 ) ; suppose len f <> 1 ; ::_thesis: mid (f,(len f),1) = Rev f then 1 < len f by A1, XXREAL_0:1; then mid (f,(len f),1) = Rev ((f /^ (1 -' 1)) | (((len f) -' 1) + 1)) by Def3 .= Rev ((f /^ 0) | (len f)) by A1, A2, XREAL_1:235 .= Rev (f | (len f)) by FINSEQ_5:28 .= Rev f by FINSEQ_1:58 ; hence mid (f,(len f),1) = Rev f ; ::_thesis: verum end; supposeA3: len f = 1 ; ::_thesis: mid (f,(len f),1) = Rev f then A4: f | 1 = f by FINSEQ_1:58; mid (f,(len f),1) = (f /^ (1 -' 1)) | ((1 -' 1) + 1) by A3, Def3 .= f | 1 by A2, FINSEQ_5:28 ; hence mid (f,(len f),1) = Rev f by A1, A4, Th110, FINSEQ_1:59; ::_thesis: verum end; end; end; theorem Th122: :: FINSEQ_6:122 for D being non empty set for f being FinSequence of D for k1, k2, i being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2, i being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) let f be FinSequence of D; ::_thesis: for k1, k2, i being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) let k1, k2, i be Element of NAT ; ::_thesis: ( 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) implies ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) ) assume that A1: 1 <= k1 and A2: k1 <= k2 and A3: k2 <= len f and A4: 1 <= i and A5: ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) ; ::_thesis: ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) A6: k1 <= len f by A2, A3, XXREAL_0:2; i + k1 >= 1 + k1 by A4, XREAL_1:6; then A7: (i + k1) - 1 >= (1 + k1) - 1 by XREAL_1:9; A8: ( i <= (k2 - k1) + 1 implies i <= (k2 -' k1) + 1 ) by A2, XREAL_1:233; i - 1 >= 1 - 1 by A4, XREAL_1:9; then A9: (i -' 1) + k1 = (i - 1) + k1 by XREAL_0:def_2 .= (i + k1) -' 1 by A7, XREAL_0:def_2 ; A10: 1 <= k2 by A1, A2, XXREAL_0:2; then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A1, A2, A3, A6, Th118; hence A11: ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) ) by A1, A2, A3, A4, A5, A10, A6, A8, A9, Th118; ::_thesis: ( (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) hence (mid (f,k1,k2)) . i = f . ((i + k1) - 1) by A7, XREAL_0:def_2; ::_thesis: (mid (f,k1,k2)) . i = f . ((i - 1) + k1) thus (mid (f,k1,k2)) . i = f . ((i - 1) + k1) by A4, A11, XREAL_1:233; ::_thesis: verum end; theorem :: FINSEQ_6:123 for D being non empty set for f being FinSequence of D for k, i being Nat st 1 <= i & i <= k & k <= len f holds (mid (f,1,k)) . i = f . i proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k, i being Nat st 1 <= i & i <= k & k <= len f holds (mid (f,1,k)) . i = f . i let f be FinSequence of D; ::_thesis: for k, i being Nat st 1 <= i & i <= k & k <= len f holds (mid (f,1,k)) . i = f . i let k, i be Nat; ::_thesis: ( 1 <= i & i <= k & k <= len f implies (mid (f,1,k)) . i = f . i ) assume that A1: 1 <= i and A2: i <= k and A3: k <= len f ; ::_thesis: (mid (f,1,k)) . i = f . i A4: i <= (k - 1) + 1 by A2; A5: k in NAT by ORDINAL1:def_12; A6: i in NAT by ORDINAL1:def_12; 1 <= k by A1, A2, XXREAL_0:2; then (mid (f,1,k)) . i = f . ((i + 1) -' 1) by A1, A3, A6, A5, A4, Th122; hence (mid (f,1,k)) . i = f . i by NAT_D:34; ::_thesis: verum end; theorem :: FINSEQ_6:124 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds len (mid (f,k1,k2)) <= len f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds len (mid (f,k1,k2)) <= len f let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds len (mid (f,k1,k2)) <= len f let k1, k2 be Element of NAT ; ::_thesis: ( 1 <= k1 & k1 <= k2 & k2 <= len f implies len (mid (f,k1,k2)) <= len f ) assume that A1: 1 <= k1 and A2: k1 <= k2 and A3: k2 <= len f ; ::_thesis: len (mid (f,k1,k2)) <= len f A4: k1 <= len f by A2, A3, XXREAL_0:2; k2 - k1 >= 0 by A2, XREAL_1:48; then A5: (k2 -' k1) + 1 = (k2 - k1) + 1 by XREAL_0:def_2 .= k2 - (k1 - 1) ; k2 <= k2 + (k1 -' 1) by NAT_1:11; then A6: k2 - (k1 -' 1) <= (k2 + (k1 -' 1)) - (k1 -' 1) by XREAL_1:9; k1 - 1 >= 0 by A1, XREAL_1:48; then A7: k1 - 1 = k1 -' 1 by XREAL_0:def_2; 1 <= k2 by A1, A2, XXREAL_0:2; then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A1, A2, A3, A4, Th118; hence len (mid (f,k1,k2)) <= len f by A3, A5, A7, A6, XXREAL_0:2; ::_thesis: verum end; theorem Th125: :: FINSEQ_6:125 for D being non empty set for f being FinSequence of D for k being Element of NAT for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k being Element of NAT for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) let f be FinSequence of D; ::_thesis: for k being Element of NAT for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) let k be Element of NAT ; ::_thesis: for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) let p be Element of D; ::_thesis: (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) A1: f | (Seg k) = f | k by FINSEQ_1:def_15; thus (<*p*> ^ f) | (k + 1) = (<*p*> ^ f) | (Seg (k + 1)) by FINSEQ_1:def_15 .= (<*p*> ^ f) | (Seg (k + (len <*p*>))) by FINSEQ_1:39 .= <*p*> ^ (f | k) by A1, Th14 ; ::_thesis: verum end; theorem :: FINSEQ_6:126 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) let k1, k2 be Element of NAT ; ::_thesis: ( k1 < k2 & k1 in dom f implies mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) ) assume A1: k1 < k2 ; ::_thesis: ( not k1 in dom f or mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) ) then A2: k1 + 1 <= k2 by NAT_1:13; A3: 1 <= k2 -' k1 proof percases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A2, XXREAL_0:1; suppose k1 + 1 = k2 ; ::_thesis: 1 <= k2 -' k1 hence 1 <= k2 -' k1 by NAT_D:34; ::_thesis: verum end; supposeA4: k1 + 1 < k2 ; ::_thesis: 1 <= k2 -' k1 ( k2 -' k1 <= 1 implies k2 <= 1 + k1 ) proof assume k2 -' k1 <= 1 ; ::_thesis: k2 <= 1 + k1 then (k2 -' k1) + k1 <= 1 + k1 by XREAL_1:6; hence k2 <= 1 + k1 by A1, XREAL_1:235; ::_thesis: verum end; hence 1 <= k2 -' k1 by A4; ::_thesis: verum end; end; end; then k2 -' k1 = k2 - k1 by NAT_D:39; then A5: (k2 -' k1) -' 1 = (k2 - k1) - 1 by A3, XREAL_1:233 .= k2 - (k1 + 1) .= k2 -' (k1 + 1) by A2, XREAL_1:233 ; assume A6: k1 in dom f ; ::_thesis: mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) then A7: f . k1 = f /. k1 by PARTFUN1:def_6; 1 <= k1 by A6, FINSEQ_3:25; then (k1 -' 1) + 1 = k1 by XREAL_1:235; then f /^ (k1 -' 1) = <*(f /. k1)*> ^ (f /^ k1) by A6, FINSEQ_5:31; hence mid (f,k1,k2) = (<*(f /. k1)*> ^ (f /^ k1)) | ((k2 -' k1) + 1) by A1, Def3 .= <*(f . k1)*> ^ ((f /^ k1) | (k2 -' k1)) by A7, Th125 .= <*(f . k1)*> ^ ((f /^ k1) | ((k2 -' (k1 + 1)) + 1)) by A3, A5, XREAL_1:235 .= <*(f . k1)*> ^ ((f /^ ((k1 + 1) -' 1)) | ((k2 -' (k1 + 1)) + 1)) by NAT_D:34 .= <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) by A2, Def3 ; ::_thesis: verum end;