:: 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;