:: FINSEQ_5 semantic presentation
begin
theorem Th1: :: FINSEQ_5:1
for i, n being Nat st i <= n holds
(n - i) + 1 is Element of NAT
proof
let i, n be Nat; ::_thesis: ( i <= n implies (n - i) + 1 is Element of NAT )
assume i <= n ; ::_thesis: (n - i) + 1 is Element of NAT
then reconsider ni = n - i as Element of NAT by INT_1:5;
ni + 1 is Element of NAT ;
hence (n - i) + 1 is Element of NAT ; ::_thesis: verum
end;
theorem Th2: :: FINSEQ_5:2
for i, n being Nat st i in Seg n holds
(n - i) + 1 in Seg n
proof
let i, n be Nat; ::_thesis: ( i in Seg n implies (n - i) + 1 in Seg n )
assume A1: i in Seg n ; ::_thesis: (n - i) + 1 in Seg n
then i <= n by FINSEQ_1:1;
then reconsider ni = n - i as Element of NAT by INT_1:5;
reconsider j = ni + 1 as Element of NAT ;
A2: now__::_thesis:_not_j_=_n_+_1
assume j = n + 1 ; ::_thesis: contradiction
then - 0 = - i ;
hence contradiction by A1, FINSEQ_1:1; ::_thesis: verum
end;
ni <= n by XREAL_1:43;
then j <= n + 1 by XREAL_1:6;
then j < n + 1 by A2, XXREAL_0:1;
then ( 0 + 1 <= j & j <= n ) by NAT_1:13;
hence (n - i) + 1 in Seg n ; ::_thesis: verum
end;
theorem Th3: :: FINSEQ_5:3
for f being Function
for x, y being set st f " {y} = {x} holds
( x in dom f & y in rng f & f . x = y )
proof
let f be Function; ::_thesis: for x, y being set st f " {y} = {x} holds
( x in dom f & y in rng f & f . x = y )
let x, y be set ; ::_thesis: ( f " {y} = {x} implies ( x in dom f & y in rng f & f . x = y ) )
assume f " {y} = {x} ; ::_thesis: ( x in dom f & y in rng f & f . x = y )
then A1: x in f " {y} by TARSKI:def_1;
hence A2: x in dom f by FUNCT_1:def_7; ::_thesis: ( y in rng f & f . x = y )
f . x in {y} by A1, FUNCT_1:def_7;
then f . x = y by TARSKI:def_1;
hence ( y in rng f & f . x = y ) by A2, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: FINSEQ_5:4
for f being Function holds
( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} )
proof
let f be Function; ::_thesis: ( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} )
now__::_thesis:_(_(_(_for_x_being_set_st_x_in_dom_f_holds_
f_is_one-to-one_at_x_)_implies_for_x_being_set_st_x_in_dom_f_holds_
f_"_{(f_._x)}_=_{x}_)_&_(_(_for_x_being_set_st_x_in_dom_f_holds_
f_"_{(f_._x)}_=_{x}_)_implies_for_x_being_set_st_x_in_dom_f_holds_
f_is_one-to-one_at_x_)_)
hereby ::_thesis: ( ( for x being set st x in dom f holds
f " {(f . x)} = {x} ) implies for x being set st x in dom f holds
f is_one-to-one_at x )
assume A1: for x being set st x in dom f holds
f is_one-to-one_at x ; ::_thesis: for x being set st x in dom f holds
f " {(f . x)} = {x}
let x be set ; ::_thesis: ( x in dom f implies f " {(f . x)} = {x} )
assume x in dom f ; ::_thesis: f " {(f . x)} = {x}
then f is_one-to-one_at x by A1;
hence f " {(f . x)} = {x} by FINSEQ_4:2; ::_thesis: verum
end;
assume A2: for x being set st x in dom f holds
f " {(f . x)} = {x} ; ::_thesis: for x being set st x in dom f holds
f is_one-to-one_at x
let x be set ; ::_thesis: ( x in dom f implies f is_one-to-one_at x )
assume A3: x in dom f ; ::_thesis: f is_one-to-one_at x
then f " {(f . x)} = {x} by A2;
hence f is_one-to-one_at x by A3, FINSEQ_4:2; ::_thesis: verum
end;
hence ( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} ) by FINSEQ_4:4; ::_thesis: verum
end;
theorem :: FINSEQ_5:5
for f being Function
for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds
y1 = y2
proof
let f be Function; ::_thesis: for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( f is one-to-one & y1 in rng f & f " {y1} = f " {y2} implies y1 = y2 )
assume that
A1: ( f is one-to-one & y1 in rng f ) and
A2: f " {y1} = f " {y2} ; ::_thesis: y1 = y2
consider x1 being set such that
A3: f " {y1} = {x1} by A1, FUNCT_1:74;
f . x1 = y1 by A3, Th3;
hence y1 = y2 by A2, A3, Th3; ::_thesis: verum
end;
registration
let x be set ;
cluster<*x*> -> trivial ;
coherence
<*x*> is trivial ;
let y be set ;
cluster<*x,y*> -> non trivial ;
coherence
not <*x,y*> is trivial
proof
len <*x,y*> = 2 by FINSEQ_1:44;
hence not <*x,y*> is trivial by NAT_D:60; ::_thesis: verum
end;
end;
registration
cluster non empty Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & not b1 is empty )
proof
set f = <*{}*>;
<*{}*> is one-to-one by FINSEQ_3:93;
hence ex b1 being FinSequence st
( b1 is one-to-one & not b1 is empty ) ; ::_thesis: verum
end;
end;
theorem Th6: :: FINSEQ_5:6
for f being non empty FinSequence holds
( 1 in dom f & len f in dom f )
proof
let f be non empty FinSequence; ::_thesis: ( 1 in dom f & len f in dom f )
A1: len f >= 1 by NAT_1:14;
hence 1 in dom f by FINSEQ_3:25; ::_thesis: len f in dom f
thus len f in dom f by A1, FINSEQ_3:25; ::_thesis: verum
end;
theorem :: FINSEQ_5:7
for f being non empty FinSequence ex i being Nat st i + 1 = len f by NAT_1:6;
theorem Th8: :: FINSEQ_5:8
for x being set
for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)
proof
let x be set ; ::_thesis: for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)
let f be FinSequence; ::_thesis: len (<*x*> ^ f) = 1 + (len f)
thus len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22
.= 1 + (len f) by FINSEQ_1:39 ; ::_thesis: verum
end;
theorem :: FINSEQ_5:9
for f being FinSequence
for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds
p = q
proof
let f be FinSequence; ::_thesis: for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds
p = q
let p, q be set ; ::_thesis: ( p in rng f & q in rng f & p .. f = q .. f implies p = q )
assume that
A1: p in rng f and
A2: q in rng f ; ::_thesis: ( not p .. f = q .. f or p = q )
assume p .. f = q .. f ; ::_thesis: p = q
hence p = f . (q .. f) by A1, FINSEQ_4:19
.= q by A2, FINSEQ_4:19 ;
::_thesis: verum
end;
theorem Th10: :: FINSEQ_5:10
for n being Nat
for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>
proof
let n be Nat; ::_thesis: for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>
let f, g be FinSequence; ::_thesis: ( n + 1 in dom f & g = f | (Seg n) implies f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> )
assume that
A1: n + 1 in dom f and
A2: g = f | (Seg n) ; ::_thesis: f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>
reconsider h = f | (Seg (n + 1)) as FinSequence by FINSEQ_1:15;
n + 1 <= len f by A1, FINSEQ_3:25;
then A3: len h = n + 1 by FINSEQ_1:17;
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then ( h . (n + 1) = f . (n + 1) & g = h | (Seg n) ) by A2, FINSEQ_1:4, FUNCT_1:49, FUNCT_1:51;
hence f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> by A3, FINSEQ_3:55; ::_thesis: verum
end;
theorem Th11: :: FINSEQ_5:11
for i being Nat
for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i
proof
let i be Nat; ::_thesis: for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i
let f be one-to-one FinSequence; ::_thesis: ( i in dom f implies (f . i) .. f = i )
assume A1: i in dom f ; ::_thesis: (f . i) .. f = i
then f . i in rng f by FUNCT_1:def_3;
then A2: f just_once_values f . i by FINSEQ_4:8;
then f <- (f . i) = (f . i) .. f by FINSEQ_4:25;
hence (f . i) .. f = i by A1, A2, FINSEQ_4:def_3; ::_thesis: verum
end;
registration
let D be non empty set ;
cluster non empty Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like for FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is one-to-one & not b1 is empty )
proof
set x = the Element of D;
set f = <* the Element of D*>;
<* the Element of D*> is one-to-one by FINSEQ_3:93;
hence ex b1 being FinSequence of D st
( b1 is one-to-one & not b1 is empty ) ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_5:12
for D being non empty set
for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds
f /. i = g /. i ) holds
f = g
proof
let D be non empty set ; ::_thesis: for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds
f /. i = g /. i ) holds
f = g
let f, g be FinSequence of D; ::_thesis: ( dom f = dom g & ( for i being Nat st i in dom f holds
f /. i = g /. i ) implies f = g )
assume that
A1: dom f = dom g and
A2: for i being Nat st i in dom f holds
f /. i = g /. i ; ::_thesis: f = g
now__::_thesis:_for_k_being_Nat_st_k_in_dom_f_holds_
f_._k_=_g_._k
let k be Nat; ::_thesis: ( k in dom f implies f . k = g . k )
assume A3: k in dom f ; ::_thesis: f . k = g . k
hence f . k = f /. k by PARTFUN1:def_6
.= g /. k by A2, A3
.= g . k by A1, A3, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence f = g by A1, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th13: :: FINSEQ_5:13
for D being non empty set
for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) holds
f = g
proof
let D be non empty set ; ::_thesis: for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) holds
f = g
let f, g be FinSequence of D; ::_thesis: ( len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) implies f = g )
assume that
A1: len f = len g and
A2: for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ; ::_thesis: f = g
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_f_holds_
f_._k_=_g_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len f implies f . k = g . k )
assume A3: ( 1 <= k & k <= len f ) ; ::_thesis: f . k = g . k
hence f . k = f /. k by FINSEQ_4:15
.= g /. k by A2, A3
.= g . k by A1, A3, FINSEQ_4:15 ;
::_thesis: verum
end;
hence f = g by A1, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th14: :: FINSEQ_5:14
for D being non empty set
for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>
let f be FinSequence of D; ::_thesis: ( len f = 1 implies f = <*(f /. 1)*> )
assume A1: len f = 1 ; ::_thesis: f = <*(f /. 1)*>
then not f is empty ;
then 1 in dom f by Th6;
then f . 1 = f /. 1 by PARTFUN1:def_6;
hence f = <*(f /. 1)*> by A1, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th15: :: FINSEQ_5:15
for D being non empty set
for p being Element of D
for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p
proof
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p
let p be Element of D; ::_thesis: for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p
let f be FinSequence of D; ::_thesis: (<*p*> ^ f) /. 1 = p
len (<*p*> ^ f) = 1 + (len f) by Th8;
then 1 <= len (<*p*> ^ f) by NAT_1:11;
then 1 in dom (<*p*> ^ f) by FINSEQ_3:25;
then (<*p*> ^ f) /. 1 = (<*p*> ^ f) . 1 by PARTFUN1:def_6;
hence (<*p*> ^ f) /. 1 = p by FINSEQ_1:41; ::_thesis: verum
end;
Lm1: for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
proof
let i be Nat; ::_thesis: for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
let D be non empty set ; ::_thesis: for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
let f, g be FinSequence of D; ::_thesis: ( i in dom f implies (f ^ g) /. i = f /. i )
assume A1: i in dom f ; ::_thesis: (f ^ g) /. i = f /. i
dom f c= dom (f ^ g) by FINSEQ_1:26;
hence (f ^ g) /. i = (f ^ g) . i by A1, PARTFUN1:def_6
.= f . i by A1, FINSEQ_1:def_7
.= f /. i by A1, PARTFUN1:def_6 ;
::_thesis: verum
end;
theorem Th16: :: FINSEQ_5:16
for f being FinSequence
for i being Nat holds len (f | i) <= len f
proof
let f be FinSequence; ::_thesis: for i being Nat holds len (f | i) <= len f
let i be Nat; ::_thesis: len (f | i) <= len f
( i <= len f implies len (f | i) = i ) by FINSEQ_1:59;
hence len (f | i) <= len f by FINSEQ_1:58; ::_thesis: verum
end;
theorem Th17: :: FINSEQ_5:17
for f being FinSequence
for i being Nat holds len (f | i) <= i
proof
let f be FinSequence; ::_thesis: for i being Nat holds len (f | i) <= i
let i be Nat; ::_thesis: len (f | i) <= i
( i <= len f implies len (f | i) = i ) by FINSEQ_1:59;
hence len (f | i) <= i by FINSEQ_1:58; ::_thesis: verum
end;
theorem Th18: :: FINSEQ_5:18
for f being FinSequence
for i being Nat holds dom (f | i) c= dom f
proof
let f be FinSequence; ::_thesis: for i being Nat holds dom (f | i) c= dom f
let i be Nat; ::_thesis: dom (f | i) c= dom f
f | i c= f by RELAT_1:59;
hence dom (f | i) c= dom f by RELAT_1:11; ::_thesis: verum
end;
theorem Th19: :: FINSEQ_5:19
for f being FinSequence
for i being Nat holds rng (f | i) c= rng f
proof
let f be FinSequence; ::_thesis: for i being Nat holds rng (f | i) c= rng f
let i be Nat; ::_thesis: rng (f | i) c= rng f
f | i c= f by RELAT_1:59;
hence rng (f | i) c= rng f by RELAT_1:11; ::_thesis: verum
end;
theorem Th20: :: FINSEQ_5:20
for D being set
for f being FinSequence of D st not f is empty holds
f | 1 = <*(f /. 1)*>
proof
let D be set ; ::_thesis: for f being FinSequence of D st not f is empty holds
f | 1 = <*(f /. 1)*>
let f be FinSequence of D; ::_thesis: ( not f is empty implies f | 1 = <*(f /. 1)*> )
assume not f is empty ; ::_thesis: f | 1 = <*(f /. 1)*>
then 1 in dom f by Th6;
then 1 <= len f by FINSEQ_3:25;
then A1: len (f | 1) = 1 by FINSEQ_1:59;
then 1 in dom (f | 1) by FINSEQ_3:25;
then ( (f | 1) /. 1 = (f | 1) . 1 & f /. 1 = (f | 1) /. 1 ) by FINSEQ_4:70, PARTFUN1:def_6;
hence f | 1 = <*(f /. 1)*> by A1, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: FINSEQ_5:21
for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>
let D be non empty set ; ::_thesis: for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>
let f be FinSequence of D; ::_thesis: ( i + 1 = len f implies f = (f | i) ^ <*(f /. (len f))*> )
assume A1: i + 1 = len f ; ::_thesis: f = (f | i) ^ <*(f /. (len f))*>
then not f is empty ;
then A2: i + 1 in dom f by A1, Th6;
dom f = Seg (i + 1) by A1, FINSEQ_1:def_3;
hence f = f | (Seg (i + 1)) by RELAT_1:68
.= (f | i) ^ <*(f . (i + 1))*> by A2, Th10
.= (f | i) ^ <*(f /. (len f))*> by A1, A2, PARTFUN1:def_6 ;
::_thesis: verum
end;
Lm2: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
let f be FinSequence of D; ::_thesis: ( f is one-to-one implies f | i is one-to-one )
assume A1: f is one-to-one ; ::_thesis: f | i is one-to-one
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_in_dom_(f_|_i)_&_m_in_dom_(f_|_i)_&_(f_|_i)_/._n_=_(f_|_i)_/._m_holds_
n_=_m
A2: dom (f | i) c= dom f by Th18;
let n, m be Element of NAT ; ::_thesis: ( n in dom (f | i) & m in dom (f | i) & (f | i) /. n = (f | i) /. m implies n = m )
assume that
A3: n in dom (f | i) and
A4: m in dom (f | i) and
A5: (f | i) /. n = (f | i) /. m ; ::_thesis: n = m
f /. n = (f | i) /. n by A3, FINSEQ_4:70
.= f /. m by A4, A5, FINSEQ_4:70 ;
hence n = m by A1, A3, A4, A2, PARTFUN2:10; ::_thesis: verum
end;
hence f | i is one-to-one by PARTFUN2:9; ::_thesis: verum
end;
registration
let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
clusterf | i -> one-to-one ;
coherence
f | i is one-to-one by Lm2;
end;
theorem Th22: :: FINSEQ_5:22
for i being Nat
for D being set
for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i
proof
let i be Nat; ::_thesis: for D being set
for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i
let D be set ; ::_thesis: for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i
let f, g be FinSequence of D; ::_thesis: ( i <= len f implies (f ^ g) | i = f | i )
assume A1: i <= len f ; ::_thesis: (f ^ g) | i = f | i
then A2: len (f | i) = i by FINSEQ_1:59;
then A3: dom (f | i) = Seg i by FINSEQ_1:def_3;
A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(f_|_i)_holds_
((f_^_g)_|_i)_._j_=_(f_|_i)_._j
let j be Nat; ::_thesis: ( j in dom (f | i) implies ((f ^ g) | i) . j = (f | i) . j )
assume A5: j in dom (f | i) ; ::_thesis: ((f ^ g) | i) . j = (f | i) . j
then j <= i by A3, FINSEQ_1:1;
then A6: j <= len f by A1, XXREAL_0:2;
( j in NAT & 1 <= j ) by A3, A5, FINSEQ_1:1;
then j in Seg (len f) by A6;
then A7: j in dom f by FINSEQ_1:def_3;
thus ((f ^ g) | i) . j = (f ^ g) . j by A3, A5, FUNCT_1:49
.= f . j by A7, FINSEQ_1:def_7
.= (f | i) . j by A3, A5, FUNCT_1:49 ; ::_thesis: verum
end;
i <= (len f) + (len g) by A1, NAT_1:12;
then i <= len (f ^ g) by FINSEQ_1:22;
then len ((f ^ g) | i) = i by FINSEQ_1:59;
hence (f ^ g) | i = f | i by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
theorem :: FINSEQ_5:23
for D being set
for f, g being FinSequence of D holds (f ^ g) | (len f) = f
proof
let D be set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) | (len f) = f
let f, g be FinSequence of D; ::_thesis: (f ^ g) | (len f) = f
thus f = f | (len f) by FINSEQ_2:20
.= (f ^ g) | (len f) by Th22 ; ::_thesis: verum
end;
theorem :: FINSEQ_5:24
for D being non empty set
for p being Element of D
for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
proof
let D be non empty set ; ::_thesis: for p being Element of D
for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let p be Element of D; ::_thesis: for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let D be set ; ::_thesis: for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -| p) ^ <*p*> = f | (p .. f) )
assume A1: p in rng f ; ::_thesis: (f -| p) ^ <*p*> = f | (p .. f)
then consider n being Nat such that
A2: n = (p .. f) - 1 and
A3: f -| p = f | (Seg n) by FINSEQ_4:def_5;
( n + 1 in dom f & f . (n + 1) = p ) by A1, A2, FINSEQ_4:19, FINSEQ_4:20;
hence (f -| p) ^ <*p*> = f | (p .. f) by A2, A3, Th10; ::_thesis: verum
end;
theorem :: FINSEQ_5:25
for i being Nat
for D being non empty set
for f being FinSequence of D holds len (f /^ i) <= len f
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D holds len (f /^ i) <= len f
let D be non empty set ; ::_thesis: for f being FinSequence of D holds len (f /^ i) <= len f
let f be FinSequence of D; ::_thesis: len (f /^ i) <= len f
percases ( i <= len f or len f < i ) ;
suppose i <= len f ; ::_thesis: len (f /^ i) <= len f
then len (f /^ i) = (len f) - i by RFINSEQ:def_1;
then (len (f /^ i)) + i = len f ;
hence len (f /^ i) <= len f by NAT_1:11; ::_thesis: verum
end;
suppose len f < i ; ::_thesis: len (f /^ i) <= len f
then f /^ i = <*> D by RFINSEQ:def_1;
hence len (f /^ i) <= len f ; ::_thesis: verum
end;
end;
end;
theorem Th26: :: FINSEQ_5:26
for i, n being Nat
for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f
proof
let i, n be Nat; ::_thesis: for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f
let D be set ; ::_thesis: for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f
let f be FinSequence of D; ::_thesis: ( i in dom (f /^ n) implies n + i in dom f )
assume A1: i in dom (f /^ n) ; ::_thesis: n + i in dom f
percases ( n <= len f or n > len f ) ;
supposeA2: n <= len f ; ::_thesis: n + i in dom f
i <= len (f /^ n) by A1, FINSEQ_3:25;
then i <= (len f) - n by A2, RFINSEQ:def_1;
then A3: n + i <= len f by XREAL_1:19;
( 1 <= i & i <= i + n ) by A1, FINSEQ_3:25, NAT_1:11;
then 1 <= i + n by XXREAL_0:2;
hence n + i in dom f by A3, FINSEQ_3:25; ::_thesis: verum
end;
suppose n > len f ; ::_thesis: n + i in dom f
then f /^ n = <*> D by RFINSEQ:def_1;
hence n + i in dom f by A1; ::_thesis: verum
end;
end;
end;
theorem Th27: :: FINSEQ_5:27
for i, n being Nat
for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)
proof
let i, n be Nat; ::_thesis: for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)
let D be set ; ::_thesis: for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)
let f be FinSequence of D; ::_thesis: ( i in dom (f /^ n) implies (f /^ n) /. i = f /. (n + i) )
assume A1: i in dom (f /^ n) ; ::_thesis: (f /^ n) /. i = f /. (n + i)
percases ( n <= len f or n > len f ) ;
supposeA2: n <= len f ; ::_thesis: (f /^ n) /. i = f /. (n + i)
A3: n + i in dom f by A1, Th26;
thus (f /^ n) /. i = (f /^ n) . i by A1, PARTFUN1:def_6
.= f . (n + i) by A1, A2, RFINSEQ:def_1
.= f /. (n + i) by A3, PARTFUN1:def_6 ; ::_thesis: verum
end;
suppose n > len f ; ::_thesis: (f /^ n) /. i = f /. (n + i)
then f /^ n = <*> D by RFINSEQ:def_1;
hence (f /^ n) /. i = f /. (n + i) by A1; ::_thesis: verum
end;
end;
end;
theorem Th28: :: FINSEQ_5:28
for D being set
for f being FinSequence of D holds f /^ 0 = f
proof
let D be set ; ::_thesis: for f being FinSequence of D holds f /^ 0 = f
let f be FinSequence of D; ::_thesis: f /^ 0 = f
A1: 0 <= len f ;
A2: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(f_/^_0)_holds_
(f_/^_0)_._i_=_f_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (f /^ 0) implies (f /^ 0) . i = f . i )
assume ( 1 <= i & i <= len (f /^ 0) ) ; ::_thesis: (f /^ 0) . i = f . i
then i in dom (f /^ 0) by FINSEQ_3:25;
hence (f /^ 0) . i = f . (i + 0) by A1, RFINSEQ:def_1
.= f . i ;
::_thesis: verum
end;
len (f /^ 0) = (len f) - 0 by RFINSEQ:def_1
.= len f ;
hence f /^ 0 = f by A2, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: FINSEQ_5:29
for D being non empty set
for f being FinSequence of D st not f is empty holds
f = <*(f /. 1)*> ^ (f /^ 1)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D st not f is empty holds
f = <*(f /. 1)*> ^ (f /^ 1)
let f be FinSequence of D; ::_thesis: ( not f is empty implies f = <*(f /. 1)*> ^ (f /^ 1) )
assume not f is empty ; ::_thesis: f = <*(f /. 1)*> ^ (f /^ 1)
then f | 1 = <*(f /. 1)*> by Th20;
hence f = <*(f /. 1)*> ^ (f /^ 1) by RFINSEQ:8; ::_thesis: verum
end;
theorem :: FINSEQ_5:30
for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>
let D be non empty set ; ::_thesis: for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>
let f be FinSequence of D; ::_thesis: ( i + 1 = len f implies f /^ i = <*(f /. (len f))*> )
assume A1: i + 1 = len f ; ::_thesis: f /^ i = <*(f /. (len f))*>
then i <= len f by NAT_1:11;
then A2: len (f /^ i) = (len f) - i by RFINSEQ:def_1
.= 1 by A1 ;
then A3: 1 in dom (f /^ i) by FINSEQ_3:25;
thus f /^ i = <*((f /^ i) /. 1)*> by A2, Th14
.= <*(f /. (len f))*> by A1, A3, Th27 ; ::_thesis: verum
end;
theorem Th31: :: FINSEQ_5:31
for j, i being Nat
for D being non empty set
for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j
proof
let j, i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j
let D be non empty set ; ::_thesis: for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j
let f be FinSequence of D; ::_thesis: ( j + 1 = i & i in dom f implies <*(f /. i)*> ^ (f /^ i) = f /^ j )
assume that
A1: j + 1 = i and
A2: i in dom f ; ::_thesis: <*(f /. i)*> ^ (f /^ i) = f /^ j
set g = <*(f /. i)*> ^ (f /^ i);
A3: i <= len f by A2, FINSEQ_3:25;
j <= i by A1, NAT_1:11;
then A4: j <= len f by A3, XXREAL_0:2;
A5: len (<*(f /. i)*> ^ (f /^ i)) = (len (f /^ i)) + 1 by Th8;
then A6: len (<*(f /. i)*> ^ (f /^ i)) = ((len f) - i) + 1 by A3, RFINSEQ:def_1
.= (len f) - j by A1
.= len (f /^ j) by A4, RFINSEQ:def_1 ;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(<*(f_/._i)*>_^_(f_/^_i))_holds_
(<*(f_/._i)*>_^_(f_/^_i))_._k_=_(f_/^_j)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) implies (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 )
assume that
A7: 1 <= k and
A8: k <= len (<*(f /. i)*> ^ (f /^ i)) ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1
A9: k in dom (f /^ j) by A6, A7, A8, FINSEQ_3:25;
percases ( k = 1 or k <> 1 ) ;
supposeA10: k = 1 ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1
hence (<*(f /. i)*> ^ (f /^ i)) . k = f /. i by FINSEQ_1:41
.= f . i by A2, PARTFUN1:def_6
.= (f /^ j) . k by A1, A4, A9, A10, RFINSEQ:def_1 ;
::_thesis: verum
end;
suppose k <> 1 ; ::_thesis: (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1
then A11: 1 < k by A7, XXREAL_0:1;
reconsider k9 = k - 1 as Element of NAT by A7, INT_1:5;
A12: k9 <= (len (<*(f /. i)*> ^ (f /^ i))) - 1 by A8, XREAL_1:9;
k9 + 1 = k ;
then 1 <= k9 by A11, NAT_1:13;
then A13: k9 in dom (f /^ i) by A5, A12, FINSEQ_3:25;
len <*(f /. i)*> = 1 by FINSEQ_1:39;
hence (<*(f /. i)*> ^ (f /^ i)) . k = (f /^ i) . k9 by A8, A11, FINSEQ_1:24
.= f . (k9 + i) by A3, A13, RFINSEQ:def_1
.= f . (k + j) by A1
.= (f /^ j) . k by A4, A9, RFINSEQ:def_1 ;
::_thesis: verum
end;
end;
end;
hence <*(f /. i)*> ^ (f /^ i) = f /^ j by A6, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th32: :: FINSEQ_5:32
for i being Nat
for D being set
for f being FinSequence of D st len f <= i holds
f /^ i is empty
proof
let i be Nat; ::_thesis: for D being set
for f being FinSequence of D st len f <= i holds
f /^ i is empty
let D be set ; ::_thesis: for f being FinSequence of D st len f <= i holds
f /^ i is empty
let f be FinSequence of D; ::_thesis: ( len f <= i implies f /^ i is empty )
assume A1: len f <= i ; ::_thesis: f /^ i is empty
percases ( len f = i or len f <> i ) ;
suppose len f = i ; ::_thesis: f /^ i is empty
then len (f /^ i) = (len f) - (len f) by RFINSEQ:def_1
.= 0 ;
hence f /^ i is empty ; ::_thesis: verum
end;
suppose len f <> i ; ::_thesis: f /^ i is empty
then len f < i by A1, XXREAL_0:1;
hence f /^ i is empty by RFINSEQ:def_1; ::_thesis: verum
end;
end;
end;
theorem Th33: :: FINSEQ_5:33
for n being Nat
for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f
proof
let n be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f
let D be non empty set ; ::_thesis: for f being FinSequence of D holds rng (f /^ n) c= rng f
let f be FinSequence of D; ::_thesis: rng (f /^ n) c= rng f
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in rng (f /^ n) or p in rng f )
assume p in rng (f /^ n) ; ::_thesis: p in rng f
then consider j being Element of NAT such that
A1: j in dom (f /^ n) and
A2: (f /^ n) /. j = p by PARTFUN2:2;
j + n in dom f by A1, Th26;
then f /. (j + n) in rng f by PARTFUN2:2;
hence p in rng f by A1, A2, Th27; ::_thesis: verum
end;
Lm3: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one
let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one
let f be FinSequence of D; ::_thesis: ( f is one-to-one implies f /^ i is one-to-one )
assume A1: f is one-to-one ; ::_thesis: f /^ i is one-to-one
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_in_dom_(f_/^_i)_&_m_in_dom_(f_/^_i)_&_(f_/^_i)_/._n_=_(f_/^_i)_/._m_holds_
n_=_m
let n, m be Element of NAT ; ::_thesis: ( n in dom (f /^ i) & m in dom (f /^ i) & (f /^ i) /. n = (f /^ i) /. m implies n = m )
assume that
A2: n in dom (f /^ i) and
A3: m in dom (f /^ i) and
A4: (f /^ i) /. n = (f /^ i) /. m ; ::_thesis: n = m
A5: ( i + n in dom f & i + m in dom f ) by A2, A3, Th26;
f /. (i + n) = (f /^ i) /. n by A2, Th27
.= f /. (i + m) by A3, A4, Th27 ;
then i + n = i + m by A1, A5, PARTFUN2:10;
hence n = m ; ::_thesis: verum
end;
hence f /^ i is one-to-one by PARTFUN2:9; ::_thesis: verum
end;
registration
let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
clusterf /^ i -> one-to-one ;
coherence
f /^ i is one-to-one by Lm3;
end;
theorem Th34: :: FINSEQ_5:34
for n being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
proof
let n be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let D be non empty set ; ::_thesis: for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let f be FinSequence of D; ::_thesis: ( f is one-to-one implies rng (f | n) misses rng (f /^ n) )
assume A1: f is one-to-one ; ::_thesis: rng (f | n) misses rng (f /^ n)
A2: dom (f | n) c= dom f by Th18;
assume rng (f | n) meets rng (f /^ n) ; ::_thesis: contradiction
then consider x being set such that
A3: x in rng (f | n) and
A4: x in rng (f /^ n) by XBOOLE_0:3;
consider i being Element of NAT such that
A5: i in dom (f | n) and
A6: (f | n) /. i = x by A3, PARTFUN2:2;
consider j being Element of NAT such that
A7: j in dom (f /^ n) and
A8: (f /^ n) /. j = x by A4, PARTFUN2:2;
A9: j + n in dom f by A7, Th26;
A10: now__::_thesis:_not_i_=_j_+_n
( i <= len (f | n) & len (f | n) <= n ) by A5, Th17, FINSEQ_3:25;
then A11: i <= n by XXREAL_0:2;
assume A12: i = j + n ; ::_thesis: contradiction
then n <= i by NAT_1:11;
then i = n by A11, XXREAL_0:1;
then j = 0 by A12;
hence contradiction by A7, FINSEQ_3:25; ::_thesis: verum
end;
f /. (j + n) = (f /^ n) /. j by A7, Th27
.= f /. i by A5, A6, A8, FINSEQ_4:70 ;
hence contradiction by A1, A5, A2, A9, A10, PARTFUN2:10; ::_thesis: verum
end;
theorem :: FINSEQ_5:35
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 .. 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 .. f)
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)
let f be FinSequence of D; ::_thesis: ( p in rng f implies f |-- p = f /^ (p .. f) )
assume A1: p in rng f ; ::_thesis: f |-- p = f /^ (p .. f)
then A2: len (f |-- p) = (len f) - (p .. f) by FINSEQ_4:def_6;
A3: p .. f <= len f by A1, FINSEQ_4:21;
then A4: len (f /^ (p .. f)) = (len f) - (p .. f) by RFINSEQ:def_1;
A5: ( Seg (len (f |-- p)) = dom (f |-- p) & Seg (len (f /^ (p .. f))) = dom (f /^ (p .. f)) ) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(f_|--_p)_holds_
(f_|--_p)_._i_=_(f_/^_(p_.._f))_._i
let i be Nat; ::_thesis: ( i in dom (f |-- p) implies (f |-- p) . i = (f /^ (p .. f)) . i )
assume A6: i in dom (f |-- p) ; ::_thesis: (f |-- p) . i = (f /^ (p .. f)) . i
hence (f |-- p) . i = f . (i + (p .. f)) by A1, FINSEQ_4:def_6
.= (f /^ (p .. f)) . i by A2, A3, A4, A5, A6, RFINSEQ:def_1 ;
::_thesis: verum
end;
hence f |-- p = f /^ (p .. f) by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th36: :: FINSEQ_5:36
for i being Nat
for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i
proof
let i be Nat; ::_thesis: for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i
let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i
let f, g be FinSequence of D; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i
A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
percases ( i <= len g or i > len g ) ;
supposeA2: i <= len g ; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i
then (len f) + i <= (len f) + (len g) by XREAL_1:6;
then A3: len ((f ^ g) /^ ((len f) + i)) = ((len g) + (len f)) - ((len f) + i) by A1, RFINSEQ:def_1
.= (len g) - i
.= len (g /^ i) by A2, RFINSEQ:def_1 ;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(g_/^_i)_holds_
((f_^_g)_/^_((len_f)_+_i))_/._k_=_(g_/^_i)_/._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (g /^ i) implies ((f ^ g) /^ ((len f) + i)) /. k = (g /^ i) /. k )
assume A4: ( 1 <= k & k <= len (g /^ i) ) ; ::_thesis: ((f ^ g) /^ ((len f) + i)) /. k = (g /^ i) /. k
then A5: k in dom (g /^ i) by FINSEQ_3:25;
then A6: i + k in dom g by Th26;
k in dom ((f ^ g) /^ ((len f) + i)) by A3, A4, FINSEQ_3:25;
hence ((f ^ g) /^ ((len f) + i)) /. k = (f ^ g) /. (((len f) + i) + k) by Th27
.= (f ^ g) /. ((len f) + (i + k))
.= g /. (i + k) by A6, FINSEQ_4:69
.= (g /^ i) /. k by A5, Th27 ;
::_thesis: verum
end;
hence (f ^ g) /^ ((len f) + i) = g /^ i by A3, Th13; ::_thesis: verum
end;
supposeA7: i > len g ; ::_thesis: (f ^ g) /^ ((len f) + i) = g /^ i
then (len f) + i > len (f ^ g) by A1, XREAL_1:6;
hence (f ^ g) /^ ((len f) + i) = <*> D by RFINSEQ:def_1
.= g /^ i by A7, RFINSEQ:def_1 ;
::_thesis: verum
end;
end;
end;
theorem :: FINSEQ_5:37
for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g
proof
let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g
let f, g be FinSequence of D; ::_thesis: (f ^ g) /^ (len f) = g
thus (f ^ g) /^ (len f) = (f ^ g) /^ ((len f) + 0)
.= g /^ 0 by Th36
.= g by Th28 ; ::_thesis: verum
end;
theorem Th38: :: FINSEQ_5:38
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
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
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
f /. (p .. f) = p
let f be FinSequence of D; ::_thesis: ( p in rng f implies f /. (p .. f) = p )
assume p in rng f ; ::_thesis: f /. (p .. f) = p
then ( p .. f in dom f & f . (p .. f) = p ) by FINSEQ_4:19, FINSEQ_4:20;
hence f /. (p .. f) = p by PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th39: :: FINSEQ_5:39
for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i
let D be non empty set ; ::_thesis: for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i
let f be FinSequence of D; ::_thesis: ( i in dom f implies (f /. i) .. f <= i )
set p = f /. i;
A1: (f /. i) .. f = (Sgm (f " {(f /. i)})) . 1 by FINSEQ_4:def_4;
f " {(f /. i)} c= dom f by RELAT_1:132;
then A2: f " {(f /. i)} c= Seg (len f) by FINSEQ_1:def_3;
assume A3: i in dom f ; ::_thesis: (f /. i) .. f <= i
then f /. i = f . i by PARTFUN1:def_6;
then f . i in {(f /. i)} by TARSKI:def_1;
then i in f " {(f /. i)} by A3, FUNCT_1:def_7;
then i in rng (Sgm (f " {(f /. i)})) by A2, FINSEQ_1:def_13;
then consider l being set such that
A4: l in dom (Sgm (f " {(f /. i)})) and
A5: (Sgm (f " {(f /. i)})) . l = i by FUNCT_1:def_3;
reconsider l = l as Element of NAT by A4;
( 1 <= l & l <= len (Sgm (f " {(f /. i)})) ) by A4, FINSEQ_3:25;
hence (f /. i) .. f <= i by A1, A2, A5, FINSEQ_3:41; ::_thesis: verum
end;
theorem :: FINSEQ_5:40
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 | i) holds
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 | i) holds
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 | i) holds
p .. (f | i) = p .. f
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f
let f be FinSequence of D; ::_thesis: ( p in rng (f | i) implies p .. (f | i) = p .. f )
A1: dom (f | i) c= dom f by Th18;
assume A2: p in rng (f | i) ; ::_thesis: p .. (f | i) = p .. f
then A3: p .. (f | i) in dom (f | i) by FINSEQ_4:20;
then f /. (p .. (f | i)) = (f | i) /. (p .. (f | i)) by FINSEQ_4:70
.= p by A2, Th38 ;
then A4: p .. f <= p .. (f | i) by A3, A1, Th39;
p .. (f | i) <= len (f | i) by A2, FINSEQ_4:21;
then A5: p .. f <= len (f | i) by A4, XXREAL_0:2;
A6: rng (f | i) c= rng f by Th19;
then 1 <= p .. f by A2, FINSEQ_4:21;
then A7: p .. f in dom (f | i) by A5, FINSEQ_3:25;
then (f | i) /. (p .. f) = f /. (p .. f) by FINSEQ_4:70
.= p by A2, A6, Th38 ;
then p .. (f | i) <= p .. f by A7, Th39;
hence p .. (f | i) = p .. f by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: FINSEQ_5:41
for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i
let D be non empty set ; ::_thesis: for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i
let f be FinSequence of D; ::_thesis: ( i in dom f & f is one-to-one implies (f /. i) .. f = i )
assume A1: i in dom f ; ::_thesis: ( not f is one-to-one or (f /. i) .. f = i )
assume f is one-to-one ; ::_thesis: (f /. i) .. f = i
then (f . i) .. f = i by A1, Th11;
hence (f /. i) .. f = i by A1, PARTFUN1:def_6; ::_thesis: verum
end;
definition
let D be non empty set ;
let f be FinSequence of D;
let p be set ;
funcf -: p -> FinSequence of D equals :: FINSEQ_5:def 1
f | (p .. f);
correctness
coherence
f | (p .. f) is FinSequence of D;
;
end;
:: deftheorem defines -: FINSEQ_5:def_1_:_
for D being non empty set
for f being FinSequence of D
for p being set holds f -: p = f | (p .. f);
theorem Th42: :: FINSEQ_5:42
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (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
len (f -: p) = p .. f
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
len (f -: p) = p .. f
let f be FinSequence of D; ::_thesis: ( p in rng f implies len (f -: p) = p .. f )
assume p in rng f ; ::_thesis: len (f -: p) = p .. f
then p .. f in dom f by FINSEQ_4:20;
then p .. f <= len f by FINSEQ_3:25;
hence len (f -: p) = p .. f by FINSEQ_1:59; ::_thesis: verum
end;
theorem Th43: :: FINSEQ_5:43
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 & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
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 & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let f be FinSequence of D; ::_thesis: ( p in rng f & i in Seg (p .. f) implies (f -: p) /. i = f /. i )
assume that
A1: p in rng f and
A2: i in Seg (p .. f) ; ::_thesis: (f -: p) /. i = f /. i
p .. f in dom f by A1, FINSEQ_4:20;
hence (f -: p) /. i = f /. i by A2, FINSEQ_4:71; ::_thesis: verum
end;
theorem :: FINSEQ_5:44
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) /. 1 = f /. 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 holds
(f -: p) /. 1 = f /. 1
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
(f -: p) /. 1 = f /. 1
let f be FinSequence of D; ::_thesis: ( p in rng f implies (f -: p) /. 1 = f /. 1 )
assume A1: p in rng f ; ::_thesis: (f -: p) /. 1 = f /. 1
then 1 <= p .. f by FINSEQ_4:21;
then 1 in Seg (p .. f) ;
hence (f -: p) /. 1 = f /. 1 by A1, Th43; ::_thesis: verum
end;
theorem :: FINSEQ_5:45
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 A1: p in rng f ; ::_thesis: (f -: p) /. (p .. f) = p
then A2: p .. f in dom f by FINSEQ_4:20;
1 <= p .. f by A1, FINSEQ_4:21;
then p .. f in Seg (p .. f) ;
hence (f -: p) /. (p .. f) = f /. (p .. f) by A1, Th43
.= f . (p .. f) by A2, PARTFUN1:def_6
.= p by A1, FINSEQ_4:19 ;
::_thesis: verum
end;
theorem :: FINSEQ_5:46
for D being non empty set
for p being Element of D
for f being FinSequence of D
for x being set st x in rng f & p in rng f & x .. f <= p .. f holds
x in rng (f -: p)
proof
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D
for x being set 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
for x being set 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: for x being set st x in rng f & p in rng f & x .. f <= p .. f holds
x in rng (f -: p)
let x be set ; ::_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)
set g = f -: p;
set i = x .. f;
1 <= x .. f by A1, FINSEQ_4:21;
then A4: x .. f in Seg (p .. f) by A3;
Seg (len (f -: p)) = dom (f -: p) by FINSEQ_1:def_3;
then A5: x .. f in dom (f -: p) by A2, A4, Th42;
then (f -: p) . (x .. f) in rng (f -: p) by FUNCT_1:def_3;
then (f -: p) /. (x .. f) in rng (f -: p) by A5, PARTFUN1:def_6;
then A6: f /. (x .. f) in rng (f -: p) by A2, A4, Th43;
x .. f in dom f by A1, FINSEQ_4:20;
then f . (x .. f) in rng (f -: p) by A6, PARTFUN1:def_6;
hence x in rng (f -: p) by A1, FINSEQ_4:19; ::_thesis: verum
end;
theorem :: FINSEQ_5:47
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
not f -: p is empty
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
not f -: p is empty
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
not f -: p is empty
let f be FinSequence of D; ::_thesis: ( p in rng f implies not f -: p is empty )
assume A1: p in rng f ; ::_thesis: not f -: p is empty
then 1 <= p .. f by FINSEQ_4:21;
then 1 <= len (f -: p) by A1, Th42;
hence not f -: p is empty ; ::_thesis: verum
end;
theorem :: FINSEQ_5:48
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (f -: p) c= rng f by Th19;
registration
let D be non empty set ;
let p be Element of D;
let f be one-to-one FinSequence of D;
clusterf -: p -> one-to-one ;
coherence
f -: p is one-to-one ;
end;
definition
let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
funcf :- p -> FinSequence of D equals :: FINSEQ_5:def 2
<*p*> ^ (f /^ (p .. f));
coherence
<*p*> ^ (f /^ (p .. f)) is FinSequence of D ;
end;
:: deftheorem defines :- FINSEQ_5:def_2_:_
for D being non empty set
for f being FinSequence of D
for p being Element of D holds f :- p = <*p*> ^ (f /^ (p .. f));
theorem Th49: :: FINSEQ_5:49
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
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
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
let f be FinSequence of D; ::_thesis: ( p in rng f implies ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) )
assume A1: p in rng f ; ::_thesis: ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
then reconsider i = (p .. f) - 1 as Element of NAT by FINSEQ_4:21, INT_1:5;
A2: p .. f in dom f by A1, FINSEQ_4:20;
take i ; ::_thesis: ( i + 1 = p .. f & f :- p = f /^ i )
thus A3: i + 1 = p .. f ; ::_thesis: f :- p = f /^ i
thus f :- p = <*(f /. (p .. f))*> ^ (f /^ (p .. f)) by A1, Th38
.= f /^ i by A3, A2, Th31 ; ::_thesis: verum
end;
theorem Th50: :: FINSEQ_5:50
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 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 holds
len (f :- p) = ((len f) - (p .. f)) + 1
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 1
let f be FinSequence of D; ::_thesis: ( p in rng f implies len (f :- p) = ((len f) - (p .. f)) + 1 )
assume A1: p in rng f ; ::_thesis: len (f :- p) = ((len f) - (p .. f)) + 1
then A2: p .. f <= len f by FINSEQ_4:21;
consider i being Element of NAT such that
A3: i + 1 = p .. f and
A4: f :- p = f /^ i by A1, Th49;
i <= p .. f by A3, NAT_1:11;
then i <= len f by A2, XXREAL_0:2;
hence len (f :- p) = (len f) - i by A4, RFINSEQ:def_1
.= ((len f) - (p .. f)) + 1 by A3 ;
::_thesis: verum
end;
theorem Th51: :: FINSEQ_5:51
for j 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 & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
proof
let j 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 & j + 1 in dom (f :- p) holds
j + (p .. f) in dom 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 & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
let f be FinSequence of D; ::_thesis: ( p in rng f & j + 1 in dom (f :- p) implies j + (p .. f) in dom f )
assume that
A1: p in rng f and
A2: j + 1 in dom (f :- p) ; ::_thesis: j + (p .. f) in dom f
j + 1 <= len (f :- p) by A2, FINSEQ_3:25;
then j + 1 <= ((len f) - (p .. f)) + 1 by A1, Th50;
then j <= (len f) - (p .. f) by XREAL_1:6;
then A3: j + (p .. f) <= len f by XREAL_1:19;
A4: p .. f <= j + (p .. f) by NAT_1:11;
1 <= p .. f by A1, FINSEQ_4:21;
then 1 <= j + (p .. f) by A4, XXREAL_0:2;
hence j + (p .. f) in dom f by A3, FINSEQ_3:25; ::_thesis: verum
end;
registration
let D be non empty set ;
let p be Element of D;
let f be FinSequence of D;
clusterf :- p -> non empty ;
coherence
not f :- p is empty ;
end;
theorem Th52: :: FINSEQ_5:52
for j 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 & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
proof
let j 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 & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (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 & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
let f be FinSequence of D; ::_thesis: ( p in rng f & j + 1 in dom (f :- p) implies (f :- p) /. (j + 1) = f /. (j + (p .. f)) )
assume that
A1: p in rng f and
A2: j + 1 in dom (f :- p) ; ::_thesis: (f :- p) /. (j + 1) = f /. (j + (p .. f))
A3: j + (p .. f) in dom f by A1, A2, Th51;
set i = j + 1;
A4: p .. f <= len f by A1, FINSEQ_4:21;
consider k being Element of NAT such that
A5: k + 1 = p .. f and
A6: f :- p = f /^ k by A1, Th49;
k <= p .. f by A5, NAT_1:11;
then A7: k <= len f by A4, XXREAL_0:2;
thus (f :- p) /. (j + 1) = (f :- p) . (j + 1) by A2, PARTFUN1:def_6
.= f . ((j + 1) + k) by A2, A6, A7, RFINSEQ:def_1
.= f /. (j + (p .. f)) by A5, A3, PARTFUN1:def_6 ; ::_thesis: verum
end;
theorem :: FINSEQ_5:53
for D being non empty set
for p being Element of D
for f being FinSequence of D holds (f :- p) /. 1 = p by Th15;
theorem :: FINSEQ_5:54
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) /. (len (f :- p)) = f /. (len 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) /. (len (f :- p)) = f /. (len f)
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
(f :- p) /. (len (f :- p)) = f /. (len f)
let f be FinSequence of D; ::_thesis: ( p in rng f implies (f :- p) /. (len (f :- p)) = f /. (len f) )
A1: len (f :- p) in dom (f :- p) by Th6;
assume A2: p in rng f ; ::_thesis: (f :- p) /. (len (f :- p)) = f /. (len f)
then p .. f <= len f by FINSEQ_4:21;
then reconsider j = (len f) - (p .. f) as Element of NAT by INT_1:5;
len (f :- p) = j + 1 by A2, Th50;
hence (f :- p) /. (len (f :- p)) = f /. (j + (p .. f)) by A2, A1, Th52
.= f /. (len f) ;
::_thesis: verum
end;
theorem :: FINSEQ_5:55
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 :- p) c= rng 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
rng (f :- p) c= rng f
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds
rng (f :- p) c= rng f
let f be FinSequence of D; ::_thesis: ( p in rng f implies rng (f :- p) c= rng f )
assume p in rng f ; ::_thesis: rng (f :- p) c= rng f
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by Th49;
hence rng (f :- p) c= rng f by Th33; ::_thesis: verum
end;
theorem :: FINSEQ_5:56
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one
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 & f is one-to-one holds
f :- p is one-to-one
let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one
let f be FinSequence of D; ::_thesis: ( p in rng f & f is one-to-one implies f :- p is one-to-one )
assume p in rng f ; ::_thesis: ( not f is one-to-one or f :- p is one-to-one )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by Th49;
hence ( not f is one-to-one or f :- p is one-to-one ) ; ::_thesis: verum
end;
definition
let f be FinSequence;
func Rev f -> FinSequence means :Def3: :: FINSEQ_5:def 3
( len it = len f & ( for i being Nat st i in dom it holds
it . i = f . (((len f) - i) + 1) ) );
existence
ex b1 being FinSequence st
( len b1 = len f & ( for i being Nat st i in dom b1 holds
b1 . i = f . (((len f) - i) + 1) ) )
proof
deffunc H1( Nat) -> set = f . (((len f) - $1) + 1);
ex p being FinSequence st
( len p = len f & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
hence ex b1 being FinSequence st
( len b1 = len f & ( for i being Nat st i in dom b1 holds
b1 . i = f . (((len f) - i) + 1) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st len b1 = len f & ( for i being Nat st i in dom b1 holds
b1 . i = f . (((len f) - i) + 1) ) & len b2 = len f & ( for i being Nat st i in dom b2 holds
b2 . i = f . (((len f) - i) + 1) ) holds
b1 = b2
proof
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
let f1, f2 be FinSequence; ::_thesis: ( len f1 = len f & ( for i being Nat st i in dom f1 holds
f1 . i = f . (((len f) - i) + 1) ) & len f2 = len f & ( for i being Nat st i in dom f2 holds
f2 . i = f . (((len f) - i) + 1) ) implies f1 = f2 )
assume that
A2: len f1 = len f and
A3: for i being Nat st i in dom f1 holds
f1 . i = f . (((len f) - i) + 1) and
A4: len f2 = len f and
A5: for i being Nat st i in dom f2 holds
f2 . i = f . (((len f) - i) + 1) ; ::_thesis: f1 = f2
A6: dom f1 = Seg (len f1) by FINSEQ_1:def_3;
A7: dom f2 = Seg (len f2) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_
f1_._i_=_f2_._i
let i be Nat; ::_thesis: ( i in dom f implies f1 . i = f2 . i )
assume A8: i in dom f ; ::_thesis: f1 . i = f2 . i
then f1 . i = f . (((len f) - i) + 1) by A2, A3, A6, A1;
hence f1 . i = f2 . i by A4, A5, A7, A1, A8; ::_thesis: verum
end;
hence f1 = f2 by A2, A4, A6, A1, FINSEQ_2:9; ::_thesis: verum
end;
involutiveness
for b1, b2 being FinSequence st len b1 = len b2 & ( for i being Nat st i in dom b1 holds
b1 . i = b2 . (((len b2) - i) + 1) ) holds
( len b2 = len b1 & ( for i being Nat st i in dom b2 holds
b2 . i = b1 . (((len b1) - i) + 1) ) )
proof
let g, f be FinSequence; ::_thesis: ( len g = len f & ( for i being Nat st i in dom g holds
g . i = f . (((len f) - i) + 1) ) implies ( len f = len g & ( for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1) ) ) )
assume that
A9: len g = len f and
A10: for i being Nat st i in dom g holds
g . i = f . (((len f) - i) + 1) ; ::_thesis: ( len f = len g & ( for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1) ) )
thus len f = len g by A9; ::_thesis: for i being Nat st i in dom f holds
f . i = g . (((len g) - i) + 1)
let i be Nat; ::_thesis: ( i in dom f implies f . i = g . (((len g) - i) + 1) )
assume A11: i in dom f ; ::_thesis: f . i = g . (((len g) - i) + 1)
then i in dom g by A9, FINSEQ_3:29;
then i <= len g by FINSEQ_3:25;
then reconsider j = (len g) - i as Element of NAT by INT_1:5;
i >= 1 by A11, FINSEQ_3:25;
then j + i >= j + 1 by XREAL_1:6;
then j + 1 <= len g ;
then j < len g by NAT_1:13;
then ( 1 <= j + 1 & j + 1 <= len g ) by NAT_1:11, NAT_1:13;
then A12: j + 1 in dom g by FINSEQ_3:25;
thus f . i = f . (((len f) - (j + 1)) + 1) by A9
.= g . (j + 1) by A10, A12
.= g . (((len g) - i) + 1) ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Rev FINSEQ_5:def_3_:_
for f, b2 being FinSequence holds
( b2 = Rev f iff ( len b2 = len f & ( for i being Nat st i in dom b2 holds
b2 . i = f . (((len f) - i) + 1) ) ) );
theorem Th57: :: FINSEQ_5:57
for f being FinSequence holds
( dom f = dom (Rev f) & rng f = rng (Rev f) )
proof
let f be FinSequence; ::_thesis: ( dom f = dom (Rev f) & rng f = rng (Rev f) )
thus A1: dom f = Seg (len f) by FINSEQ_1:def_3
.= Seg (len (Rev f)) by Def3
.= dom (Rev f) by FINSEQ_1:def_3 ; ::_thesis: rng f = rng (Rev f)
A2: len f = len (Rev f) by Def3;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng (Rev f) c= rng f
let x be set ; ::_thesis: ( x in rng f implies x in rng (Rev f) )
assume x in rng f ; ::_thesis: x in rng (Rev f)
then consider i being Nat such that
A3: i in dom f and
A4: f . i = x by FINSEQ_2:10;
i <= len f by A3, FINSEQ_3:25;
then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1;
dom f = Seg (len f) by FINSEQ_1:def_3;
then j in Seg (len (Rev f)) by A2, A3, Th2;
then A5: j in dom (Rev f) by FINSEQ_1:def_3;
then (Rev f) . j = f . (((len f) - j) + 1) by Def3;
hence x in rng (Rev f) by A4, A5, FUNCT_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rev f) or x in rng f )
assume x in rng (Rev f) ; ::_thesis: x in rng f
then consider i being Nat such that
A6: i in dom (Rev f) and
A7: (Rev f) . i = x by FINSEQ_2:10;
i <= len f by A2, A6, FINSEQ_3:25;
then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1;
i in Seg (len (Rev f)) by A6, FINSEQ_1:def_3;
then j in Seg (len (Rev f)) by A2, Th2;
then A8: j in dom (Rev f) by FINSEQ_1:def_3;
(Rev f) . i = f . (((len f) - i) + 1) by A6, Def3;
hence x in rng f by A1, A7, A8, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th58: :: FINSEQ_5:58
for i being Nat
for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)
proof
let i be Nat; ::_thesis: for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)
let f be FinSequence; ::_thesis: ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) )
dom f = dom (Rev f) by Th57;
hence ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) ) by Def3; ::_thesis: verum
end;
theorem Th59: :: FINSEQ_5:59
for f being FinSequence
for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)
proof
let f be FinSequence; ::_thesis: for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)
let i, j be Nat; ::_thesis: ( i in dom f & i + j = (len f) + 1 implies j in dom (Rev f) )
assume that
A1: i in dom f and
A2: i + j = (len f) + 1 ; ::_thesis: j in dom (Rev f)
A3: ( dom f = Seg (len f) & dom f = dom (Rev f) ) by Th57, FINSEQ_1:def_3;
j = ((len f) - i) + 1 by A2;
hence j in dom (Rev f) by A1, A3, Th2; ::_thesis: verum
end;
registration
let f be empty FinSequence;
cluster Rev f -> empty ;
coherence
Rev f is empty
proof
len {} = 0 ;
then len (Rev {}) = 0 by Def3;
hence Rev f is empty ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_5:60
for x being set holds Rev <*x*> = <*x*>
proof
let x be set ; ::_thesis: Rev <*x*> = <*x*>
set f = <*x*>;
A1: len <*x*> = 1 by FINSEQ_1:39;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*x*>_holds_
<*x*>_._i_=_<*x*>_._(((len_<*x*>)_-_i)_+_1)
let i be Nat; ::_thesis: ( i in dom <*x*> implies <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) )
assume i in dom <*x*> ; ::_thesis: <*x*> . i = <*x*> . (((len <*x*>) - i) + 1)
then i in Seg (len <*x*>) by FINSEQ_1:def_3;
then i = 1 by A1, FINSEQ_1:2, TARSKI:def_1;
hence <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) by FINSEQ_1:39; ::_thesis: verum
end;
hence Rev <*x*> = <*x*> by Def3; ::_thesis: verum
end;
theorem :: FINSEQ_5:61
for x1, x2 being set holds Rev <*x1,x2*> = <*x2,x1*>
proof
let x1, x2 be set ; ::_thesis: Rev <*x1,x2*> = <*x2,x1*>
set f = <*x1,x2*>;
set g = <*x2,x1*>;
A1: len <*x1,x2*> = 2 by FINSEQ_1:44;
A2: len <*x2,x1*> = 2 by FINSEQ_1:44;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*x2,x1*>_holds_
<*x2,x1*>_._i_=_<*x1,x2*>_._(((len_<*x1,x2*>)_-_i)_+_1)
let i be Nat; ::_thesis: ( i in dom <*x2,x1*> implies <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) )
assume i in dom <*x2,x1*> ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1)
then A3: i in Seg (len <*x1,x2*>) by A1, A2, FINSEQ_1:def_3;
percases ( i = 1 or i = 2 ) by A1, A3, FINSEQ_1:2, TARSKI:def_2;
supposeA4: i = 1 ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1)
hence <*x2,x1*> . i = x2 by FINSEQ_1:44
.= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A4, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA5: i = 2 ; ::_thesis: <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1)
hence <*x2,x1*> . i = x1 by FINSEQ_1:44
.= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A5, FINSEQ_1:44 ;
::_thesis: verum
end;
end;
end;
hence Rev <*x1,x2*> = <*x2,x1*> by A1, A2, Def3; ::_thesis: verum
end;
theorem Th62: :: FINSEQ_5:62
for f being FinSequence holds
( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )
proof
let f be FinSequence; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )
percases ( f is empty or not f is empty ) ;
supposeA1: f is empty ; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )
then A2: dom (Rev f) = {} ;
thus f . 1 = {} by A1
.= (Rev f) . (len f) by A2, FUNCT_1:def_2 ; ::_thesis: f . (len f) = (Rev f) . 1
thus f . (len f) = {} by A1
.= (Rev f) . 1 by A2, FUNCT_1:def_2 ; ::_thesis: verum
end;
supposeA3: not f is empty ; ::_thesis: ( f . 1 = (Rev f) . (len f) & f . (len f) = (Rev f) . 1 )
then len f in Seg (len f) by FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def_3;
hence (Rev f) . (len f) = f . (((len f) - (len f)) + 1) by Th58
.= f . 1 ;
::_thesis: f . (len f) = (Rev f) . 1
len f >= 1 by A3, NAT_1:14;
then 1 in dom f by FINSEQ_3:25;
hence (Rev f) . 1 = f . (((len f) - 1) + 1) by Th58
.= f . (len f) ;
::_thesis: verum
end;
end;
end;
registration
let f be one-to-one FinSequence;
cluster Rev f -> one-to-one ;
coherence
Rev f is one-to-one
proof
set g = Rev f;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (Rev f) or not x2 in dom (Rev f) or not (Rev f) . x1 = (Rev f) . x2 or x1 = x2 )
assume that
A1: x1 in dom (Rev f) and
A2: x2 in dom (Rev f) and
A3: (Rev f) . x1 = (Rev f) . x2 ; ::_thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A1, A2;
A4: len (Rev f) = len f by Def3;
then ( i1 <= len f & i2 <= len f ) by A1, A2, FINSEQ_3:25;
then reconsider i19 = ((len f) - i1) + 1, i29 = ((len f) - i2) + 1 as Element of NAT by Th1;
A5: f . i19 = (Rev f) . x1 by A1, Def3
.= f . i29 by A2, A3, Def3 ;
( dom (Rev f) = Seg (len (Rev f)) & dom f = Seg (len f) ) by FINSEQ_1:def_3;
then ( i19 in dom f & i29 in dom f ) by A1, A2, A4, Th2;
then i19 = i29 by A5, FUNCT_1:def_4;
hence x1 = x2 ; ::_thesis: verum
end;
end;
theorem Th63: :: FINSEQ_5:63
for f being FinSequence
for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
proof
let f be FinSequence; ::_thesis: for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
let x be set ; ::_thesis: Rev (f ^ <*x*>) = <*x*> ^ (Rev f)
set n = (len f) + 1;
set g = <*x*>;
A1: len (<*x*> ^ (Rev f)) = (len <*x*>) + (len (Rev f)) by FINSEQ_1:22
.= 1 + (len (Rev f)) by FINSEQ_1:39
.= (len f) + 1 by Def3 ;
A2: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_2:16;
then A3: len (Rev (f ^ <*x*>)) = (len f) + 1 by Def3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Rev_(f_^_<*x*>))_holds_
(Rev_(f_^_<*x*>))_._i_=_(<*x*>_^_(Rev_f))_._i
let i be Nat; ::_thesis: ( i in dom (Rev (f ^ <*x*>)) implies (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1 )
A4: len <*x*> = 1 by FINSEQ_1:40;
assume A5: i in dom (Rev (f ^ <*x*>)) ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1
then A6: 1 <= i by FINSEQ_3:25;
A7: i <= (len f) + 1 by A3, A5, FINSEQ_3:25;
percases ( i = 1 or i > 1 ) by A6, XXREAL_0:1;
supposeA8: i = 1 ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1
Seg (len <*x*>) = dom <*x*> by FINSEQ_1:def_3;
then A9: 1 in dom <*x*> by A4;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - 1) + 1) by A2, A5, A8, Def3
.= x by FINSEQ_1:42
.= <*x*> . 1 by FINSEQ_1:40
.= (<*x*> ^ (Rev f)) . i by A8, A9, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA10: i > 1 ; ::_thesis: (Rev (f ^ <*x*>)) . b1 = (<*x*> ^ (Rev f)) . b1
then reconsider j = i - 1 as Element of NAT by NAT_1:20;
consider l being Nat such that
A11: i = l + 1 by A10, NAT_1:6;
reconsider k = (((len f) + 1) - i) + 1 as Element of NAT by A7, Th1;
(len f) + 1 < (len f) + i by A10, XREAL_1:8;
then ((len f) + 1) - i < ((len f) + i) - i by XREAL_1:9;
then k < (len f) + 1 by XREAL_1:6;
then A12: k <= len f by NAT_1:13;
i - i <= ((len f) + 1) - i by A7, XREAL_1:9;
then 0 + 1 <= k by XREAL_1:6;
then A13: k in dom f by A12, FINSEQ_3:25;
l <> 0 by A10, A11;
then A14: 1 <= j by A11, NAT_1:14;
j <= ((len f) + 1) - 1 by A7, XREAL_1:9;
then A15: j in dom f by A14, FINSEQ_3:25;
thus (Rev (f ^ <*x*>)) . i = (f ^ <*x*>) . ((((len f) + 1) - i) + 1) by A2, A5, Def3
.= f . (((len f) - j) + 1) by A13, FINSEQ_1:def_7
.= (Rev f) . j by A15, Th58
.= (<*x*> ^ (Rev f)) . i by A1, A7, A4, A10, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence Rev (f ^ <*x*>) = <*x*> ^ (Rev f) by A1, A3, FINSEQ_2:9; ::_thesis: verum
end;
theorem :: FINSEQ_5:64
for f, g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)
proof
let f be FinSequence; ::_thesis: for g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)
defpred S1[ FinSequence] means Rev (f ^ $1) = (Rev $1) ^ (Rev f);
A1: S1[ {} ]
proof
set g = {} ;
thus Rev (f ^ {}) = Rev f by FINSEQ_1:34
.= (Rev {}) ^ (Rev f) by FINSEQ_1:34 ; ::_thesis: verum
end;
A2: for g being FinSequence
for x being set st S1[g] holds
S1[g ^ <*x*>]
proof
let g be FinSequence; ::_thesis: for x being set st S1[g] holds
S1[g ^ <*x*>]
let x be set ; ::_thesis: ( S1[g] implies S1[g ^ <*x*>] )
assume A3: S1[g] ; ::_thesis: S1[g ^ <*x*>]
thus Rev (f ^ (g ^ <*x*>)) = Rev ((f ^ g) ^ <*x*>) by FINSEQ_1:32
.= <*x*> ^ ((Rev g) ^ (Rev f)) by A3, Th63
.= (<*x*> ^ (Rev g)) ^ (Rev f) by FINSEQ_1:32
.= (Rev (g ^ <*x*>)) ^ (Rev f) by Th63 ; ::_thesis: verum
end;
thus for g being FinSequence holds S1[g] from FINSEQ_1:sch_3(A1, A2); ::_thesis: verum
end;
definition
let D be set ;
let f be FinSequence of D;
:: original: Rev
redefine func Rev f -> FinSequence of D;
coherence
Rev f is FinSequence of D
proof
set n = len f;
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Rev_f)_holds_
(Rev_f)_._i_in_D
let i be Nat; ::_thesis: ( i in dom (Rev f) implies (Rev f) . i in D )
set j = ((len f) - i) + 1;
assume i in dom (Rev f) ; ::_thesis: (Rev f) . i in D
then i in Seg (len (Rev f)) by FINSEQ_1:def_3;
then A2: i in Seg (len f) by Def3;
then ((len f) - i) + 1 in Seg (len f) by Th2;
then f . (((len f) - i) + 1) in D by A1, FINSEQ_2:11;
hence (Rev f) . i in D by A1, A2, Th58; ::_thesis: verum
end;
hence Rev f is FinSequence of D by FINSEQ_2:12; ::_thesis: verum
end;
end;
theorem :: FINSEQ_5:65
for D being non empty set
for f being FinSequence of D st not f is empty holds
( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D st not f is empty holds
( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
let f be FinSequence of D; ::_thesis: ( not f is empty implies ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 ) )
A1: dom f = dom (Rev f) by Th57;
assume A2: not f is empty ; ::_thesis: ( f /. 1 = (Rev f) /. (len f) & f /. (len f) = (Rev f) /. 1 )
then A3: len f in dom f by Th6;
1 in dom f by A2, Th6;
hence f /. 1 = f . 1 by PARTFUN1:def_6
.= (Rev f) . (len f) by Th62
.= (Rev f) /. (len f) by A3, A1, PARTFUN1:def_6 ;
::_thesis: f /. (len f) = (Rev f) /. 1
thus f /. (len f) = f . (len f) by A3, PARTFUN1:def_6
.= (Rev f) . 1 by Th62
.= (Rev f) /. 1 by A2, A1, Th6, PARTFUN1:def_6 ; ::_thesis: verum
end;
theorem :: FINSEQ_5:66
for j being Nat
for D being non empty set
for f being FinSequence of D
for i being Nat st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
proof
let j be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D
for i being Nat st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i being Nat st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
let f be FinSequence of D; ::_thesis: for i being Nat st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j
let i be Nat; ::_thesis: ( i in dom f & i + j = (len f) + 1 implies f /. i = (Rev f) /. j )
assume that
A1: i in dom f and
A2: i + j = (len f) + 1 ; ::_thesis: f /. i = (Rev f) /. j
A3: j in dom (Rev f) by A1, A2, Th59;
A4: i = ((len f) - j) + 1 by A2;
thus f /. i = f . i by A1, PARTFUN1:def_6
.= (Rev f) . j by A4, A3, Def3
.= (Rev f) /. j by A3, PARTFUN1:def_6 ; ::_thesis: verum
end;
definition
let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
let n be Nat;
func Ins (f,n,p) -> FinSequence of D equals :: FINSEQ_5:def 4
((f | n) ^ <*p*>) ^ (f /^ n);
correctness
coherence
((f | n) ^ <*p*>) ^ (f /^ n) is FinSequence of D;
;
end;
:: deftheorem defines Ins FINSEQ_5:def_4_:_
for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat holds Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n);
theorem :: FINSEQ_5:67
for D being non empty set
for p being Element of D
for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f
proof
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f
let p be Element of D; ::_thesis: for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f
let f be FinSequence of D; ::_thesis: Ins (f,0,p) = <*p*> ^ f
thus Ins (f,0,p) = <*p*> ^ (f /^ 0) by FINSEQ_1:34
.= <*p*> ^ f by Th28 ; ::_thesis: verum
end;
theorem Th68: :: FINSEQ_5:68
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>
let p be Element of D; ::_thesis: for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>
let f be FinSequence of D; ::_thesis: ( len f <= n implies Ins (f,n,p) = f ^ <*p*> )
assume A1: len f <= n ; ::_thesis: Ins (f,n,p) = f ^ <*p*>
then f /^ n is empty by Th32;
hence Ins (f,n,p) = (f | n) ^ <*p*> by FINSEQ_1:34
.= f ^ <*p*> by A1, FINSEQ_1:58 ;
::_thesis: verum
end;
theorem :: FINSEQ_5:69
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let p be Element of D; ::_thesis: for f being FinSequence of D holds len (Ins (f,n,p)) = (len f) + 1
let f be FinSequence of D; ::_thesis: len (Ins (f,n,p)) = (len f) + 1
percases ( n <= len f or len f < n ) ;
supposeA1: n <= len f ; ::_thesis: len (Ins (f,n,p)) = (len f) + 1
thus len (Ins (f,n,p)) = (len ((f | n) ^ <*p*>)) + (len (f /^ n)) by FINSEQ_1:22
.= (len ((f | n) ^ <*p*>)) + ((len f) - n) by A1, RFINSEQ:def_1
.= ((len (f | n)) + (len <*p*>)) + ((len f) - n) by FINSEQ_1:22
.= ((len (f | n)) + 1) + ((len f) - n) by FINSEQ_1:39
.= (n + 1) + ((len f) - n) by A1, FINSEQ_1:59
.= (len f) + 1 ; ::_thesis: verum
end;
suppose len f < n ; ::_thesis: len (Ins (f,n,p)) = (len f) + 1
then Ins (f,n,p) = f ^ <*p*> by Th68;
hence len (Ins (f,n,p)) = (len f) + 1 by FINSEQ_2:16; ::_thesis: verum
end;
end;
end;
theorem Th70: :: FINSEQ_5:70
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let p be Element of D; ::_thesis: for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let f be FinSequence of D; ::_thesis: rng (Ins (f,n,p)) = {p} \/ (rng f)
thus rng (Ins (f,n,p)) = (rng ((f | n) ^ <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31
.= ((rng (f | n)) \/ (rng <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31
.= ((rng (f | n)) \/ (rng (f /^ n))) \/ (rng <*p*>) by XBOOLE_1:4
.= (rng ((f | n) ^ (f /^ n))) \/ (rng <*p*>) by FINSEQ_1:31
.= (rng <*p*>) \/ (rng f) by RFINSEQ:8
.= {p} \/ (rng f) by FINSEQ_1:38 ; ::_thesis: verum
end;
registration
let D be non empty set ;
let f be FinSequence of D;
let n be Nat;
let p be Element of D;
cluster Ins (f,n,p) -> non empty ;
coherence
not Ins (f,n,p) is empty ;
end;
theorem :: FINSEQ_5:71
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))
let p be Element of D; ::_thesis: for f being FinSequence of D holds p in rng (Ins (f,n,p))
let f be FinSequence of D; ::_thesis: p in rng (Ins (f,n,p))
p in {p} by TARSKI:def_1;
then p in {p} \/ (rng f) by XBOOLE_0:def_3;
hence p in rng (Ins (f,n,p)) by Th70; ::_thesis: verum
end;
theorem Th72: :: FINSEQ_5:72
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i
let p be Element of D; ::_thesis: for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i
let f be FinSequence of D; ::_thesis: for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) /. i = f /. i
let i be Nat; ::_thesis: ( i in dom (f | n) implies (Ins (f,n,p)) /. i = f /. i )
assume A1: i in dom (f | n) ; ::_thesis: (Ins (f,n,p)) /. i = f /. i
thus (Ins (f,n,p)) /. i = ((f | n) ^ (<*p*> ^ (f /^ n))) /. i by FINSEQ_1:32
.= (f | n) /. i by A1, Lm1
.= f /. i by A1, FINSEQ_4:70 ; ::_thesis: verum
end;
theorem :: FINSEQ_5:73
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) /. (n + 1) = p
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) /. (n + 1) = p
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) /. (n + 1) = p
let p be Element of D; ::_thesis: for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) /. (n + 1) = p
let f be FinSequence of D; ::_thesis: ( n <= len f implies (Ins (f,n,p)) /. (n + 1) = p )
A1: 1 <= n + 1 by NAT_1:11;
assume n <= len f ; ::_thesis: (Ins (f,n,p)) /. (n + 1) = p
then A2: len (f | n) = n by FINSEQ_1:59;
then len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:16;
then n + 1 in dom ((f | n) ^ <*p*>) by A1, FINSEQ_3:25;
hence (Ins (f,n,p)) /. (n + 1) = ((f | n) ^ <*p*>) /. (n + 1) by Lm1
.= p by A2, FINSEQ_4:67 ;
::_thesis: verum
end;
theorem :: FINSEQ_5:74
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i
let p be Element of D; ::_thesis: for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i
let f be FinSequence of D; ::_thesis: for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) /. (i + 1) = f /. i
let i be Nat; ::_thesis: ( n + 1 <= i & i <= len f implies (Ins (f,n,p)) /. (i + 1) = f /. i )
assume that
A1: n + 1 <= i and
A2: i <= len f ; ::_thesis: (Ins (f,n,p)) /. (i + 1) = f /. i
reconsider j = i - (n + 1) as Element of NAT by A1, INT_1:5;
n + (j + 1) <= len f by A2;
then A3: j + 1 <= (len f) - n by XREAL_1:19;
n <= n + 1 by NAT_1:11;
then A4: n <= i by A1, XXREAL_0:2;
then len (f | n) = n by A2, FINSEQ_1:59, XXREAL_0:2;
then A5: len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:16;
n <= len f by A2, A4, XXREAL_0:2;
then ( 1 <= j + 1 & j + 1 <= len (f /^ n) ) by A3, NAT_1:11, RFINSEQ:def_1;
then A6: j + 1 in dom (f /^ n) by FINSEQ_3:25;
(n + 1) + (j + 1) = i + 1 ;
hence (Ins (f,n,p)) /. (i + 1) = (f /^ n) /. (j + 1) by A5, A6, FINSEQ_4:69
.= f /. (n + (j + 1)) by A6, Th27
.= f /. i ;
::_thesis: verum
end;
theorem :: FINSEQ_5:75
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1
let p be Element of D; ::_thesis: for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1
let f be FinSequence of D; ::_thesis: ( 1 <= n & not f is empty implies (Ins (f,n,p)) /. 1 = f /. 1 )
assume that
A1: 1 <= n and
A2: not f is empty ; ::_thesis: (Ins (f,n,p)) /. 1 = f /. 1
A3: ( n <= len f implies len (f | n) = n ) by FINSEQ_1:59;
1 <= len f by A2, NAT_1:14;
then 1 <= len (f | n) by A1, A3, FINSEQ_1:58;
then 1 in dom (f | n) by FINSEQ_3:25;
hence (Ins (f,n,p)) /. 1 = f /. 1 by Th72; ::_thesis: verum
end;
theorem :: FINSEQ_5:76
for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
proof
let n be Nat; ::_thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let D be non empty set ; ::_thesis: for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let p be Element of D; ::_thesis: for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let f be FinSequence of D; ::_thesis: ( f is one-to-one & not p in rng f implies Ins (f,n,p) is one-to-one )
assume that
A1: f is one-to-one and
A2: not p in rng f ; ::_thesis: Ins (f,n,p) is one-to-one
now__::_thesis:_for_x_being_set_st_x_in_rng_(f_/^_n)_holds_
not_x_in_rng_((f_|_n)_^_<*p*>)
let x be set ; ::_thesis: ( x in rng (f /^ n) implies not x in rng ((f | n) ^ <*p*>) )
assume A3: x in rng (f /^ n) ; ::_thesis: not x in rng ((f | n) ^ <*p*>)
rng (f /^ n) c= rng f by Th33;
then x in rng f by A3;
then not x in {p} by A2, TARSKI:def_1;
then A4: not x in rng <*p*> by FINSEQ_1:38;
rng (f | n) misses rng (f /^ n) by A1, Th34;
then not x in rng (f | n) by A3, XBOOLE_0:3;
then not x in (rng (f | n)) \/ (rng <*p*>) by A4, XBOOLE_0:def_3;
hence not x in rng ((f | n) ^ <*p*>) by FINSEQ_1:31; ::_thesis: verum
end;
then A5: rng ((f | n) ^ <*p*>) misses rng (f /^ n) by XBOOLE_0:3;
now__::_thesis:_for_x_being_set_st_x_in_rng_<*p*>_holds_
not_x_in_rng_(f_|_n)
let x be set ; ::_thesis: ( x in rng <*p*> implies not x in rng (f | n) )
assume x in rng <*p*> ; ::_thesis: not x in rng (f | n)
then x in {p} by FINSEQ_1:38;
then A6: not x in rng f by A2, TARSKI:def_1;
rng (f | n) c= rng f by Th19;
hence not x in rng (f | n) by A6; ::_thesis: verum
end;
then ( <*p*> is one-to-one & rng (f | n) misses rng <*p*> ) by FINSEQ_3:93, XBOOLE_0:3;
then (f | n) ^ <*p*> is one-to-one by A1, FINSEQ_3:91;
hence Ins (f,n,p) is one-to-one by A1, A5, FINSEQ_3:91; ::_thesis: verum
end;
begin
theorem :: FINSEQ_5:77
for D being non empty set
for f being FinSequence of D
for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
let f be FinSequence of D; ::_thesis: for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
let i1, i2 be Nat; ::_thesis: ( i1 <= i2 implies ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) )
assume A1: i1 <= i2 ; ::_thesis: ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
len (f | i1) <= i1 by Th17;
hence (f | i1) | i2 = f | i1 by A1, FINSEQ_1:58, XXREAL_0:2; ::_thesis: (f | i2) | i1 = f | i1
Seg i1 c= Seg i2 by A1, FINSEQ_1:5;
hence (f | i2) | i1 = f | i1 by FUNCT_1:51; ::_thesis: verum
end;
theorem :: FINSEQ_5:78
for D being non empty set
for i being Nat holds (<*> D) | i = <*> D ;
theorem :: FINSEQ_5:79
for D being non empty set holds Rev (<*> D) = <*> D ;
registration
cluster non trivial Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like for set ;
existence
not for b1 being FinSequence holds b1 is trivial
proof
take <*0,0*> ; ::_thesis: not <*0,0*> is trivial
thus not <*0,0*> is trivial ; ::_thesis: verum
end;
end;
theorem :: FINSEQ_5:80
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
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
let f be FinSequence of D; ::_thesis: for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
let l1, l2 be Nat; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
percases ( l1 <= l2 or l1 > l2 ) ;
supposeA1: l1 <= l2 ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
percases ( l2 <= len f or l2 > len f ) ;
supposeA2: l2 <= len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
then A3: l2 - l1 <= (len f) - l1 by XREAL_1:9;
A4: l1 <= len (f | l2) by A1, A2, FINSEQ_1:59;
then A5: len ((f | l2) /^ l1) = (len (f | l2)) - l1 by RFINSEQ:def_1
.= l2 - l1 by A2, FINSEQ_1:59
.= l2 -' l1 by A1, XREAL_1:233 ;
A6: l1 <= len f by A1, A2, XXREAL_0:2;
then len (f /^ l1) = (len f) - l1 by RFINSEQ:def_1;
then A7: l2 -' l1 <= len (f /^ l1) by A1, A3, XREAL_1:233;
A8: for k being Nat st 1 <= k & k <= len ((f | l2) /^ l1) holds
((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len ((f | l2) /^ l1) implies ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k )
assume that
A9: 1 <= k and
A10: k <= len ((f | l2) /^ l1) ; ::_thesis: ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k
A11: k in dom ((f | l2) /^ l1) by A9, A10, FINSEQ_3:25;
k <= l2 - l1 by A1, A5, A10, XREAL_1:233;
then A12: k + l1 <= (l2 - l1) + l1 by XREAL_1:6;
k <= len (f /^ l1) by A7, A5, A10, XXREAL_0:2;
then A13: k in dom (f /^ l1) by A9, FINSEQ_3:25;
k in NAT by ORDINAL1:def_12;
then k in Seg (l2 -' l1) by A5, A9, A10;
then ((f /^ l1) | (l2 -' l1)) . k = (f /^ l1) . k by FUNCT_1:49
.= f . (k + l1) by A6, A13, RFINSEQ:def_1
.= (f | l2) . (k + l1) by A12, FINSEQ_3:112
.= ((f | l2) /^ l1) . k by A4, A11, RFINSEQ:def_1 ;
hence ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k ; ::_thesis: verum
end;
len ((f /^ l1) | (l2 -' l1)) = l2 -' l1 by A7, FINSEQ_1:59;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A5, A8, FINSEQ_1:14; ::_thesis: verum
end;
supposeA14: l2 > len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
A15: len (f /^ l1) = (len f) -' l1 by RFINSEQ:29;
f | l2 = f by A14, FINSEQ_1:58;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A14, A15, FINSEQ_1:58, NAT_D:42; ::_thesis: verum
end;
end;
end;
supposeA16: l1 > l2 ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
reconsider l19 = l1, l29 = l2 as Element of NAT by ORDINAL1:def_12;
l1 - l1 > l2 - l1 by A16, XREAL_1:9;
then l2 -' l1 = 0 by XREAL_0:def_2;
then dom ((f /^ l1) | (l2 -' l1)) = (dom (f /^ l1)) /\ ({} NAT)
.= {} NAT ;
then A17: (f /^ l1) | (l2 -' l1) = <*> D ;
percases ( l1 <= len f or l1 > len f ) ;
suppose l1 <= len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
then l19 > len (f | l29) by A16, FINSEQ_1:59, XXREAL_0:2;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, Th32; ::_thesis: verum
end;
supposeA18: l1 > len f ; ::_thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
len (f | l29) <= len f by Th16;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, A18, Th32, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: FINSEQ_5:81
for D being set
for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>
proof
let D be set ; ::_thesis: for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>
let f be FinSequence of D; ::_thesis: ( len f >= 2 implies f | 2 = <*(f /. 1),(f /. 2)*> )
set d1 = f /. 1;
set d2 = f /. 2;
assume A1: len f >= 2 ; ::_thesis: f | 2 = <*(f /. 1),(f /. 2)*>
then A2: len (f | 2) = 2 by FINSEQ_1:59;
not D is empty by A1;
then reconsider D = D as non empty set ;
reconsider f = f as FinSequence of D ;
2 in dom (f | 2) by A2, FINSEQ_3:25;
then A4: f /. 2 = (f | 2) /. 2 by FINSEQ_4:70
.= (f | 2) . 2 by A2, FINSEQ_4:15 ;
1 in dom (f | 2) by A2, FINSEQ_3:25;
then f /. 1 = (f | 2) /. 1 by FINSEQ_4:70
.= (f | 2) . 1 by A2, FINSEQ_4:15 ;
hence f | 2 = <*(f /. 1),(f /. 2)*> by A2, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th82: :: FINSEQ_5:82
for k being Nat
for D being set
for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
proof
let k be Nat; ::_thesis: for D being set
for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
let D be set ; ::_thesis: for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
let f be FinSequence of D; ::_thesis: ( k + 1 <= len f implies f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> )
A1: 1 <= k + 1 by NAT_1:12;
assume k + 1 <= len f ; ::_thesis: f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
then A2: k + 1 in dom f by A1, FINSEQ_3:25;
then f | (Seg (k + 1)) = (f | k) ^ <*(f . (k + 1))*> by Th10;
hence f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> by A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th83: :: FINSEQ_5:83
for D being set
for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
proof
let D be set ; ::_thesis: for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
let p be FinSequence of D; ::_thesis: for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
let i be Nat; ::_thesis: ( i < len p implies p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> )
assume i < len p ; ::_thesis: p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
then A1: i + 1 <= len p by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then A2: i + 1 in dom p by A1, FINSEQ_3:25;
p | (i + 1) = (p | i) ^ <*(p /. (i + 1))*> by A1, Th82;
hence p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: FINSEQ_5:84
for D being non empty set
for p being FinSequence of D
for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
proof
let D be non empty set ; ::_thesis: for p being FinSequence of D
for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
let p be FinSequence of D; ::_thesis: for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
let n be Nat; ::_thesis: ( 1 <= n & n <= len p implies p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) )
assume that
A1: 1 <= n and
A2: n <= len p ; ::_thesis: p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)
len p >= (n -' 1) + 1 by A1, A2, XREAL_1:235;
then A3: len p > n -' 1 by NAT_1:13;
p | n = p | ((n -' 1) + 1) by A1, XREAL_1:235
.= (p | (n -' 1)) ^ <*(p . ((n -' 1) + 1))*> by A3, Th83
.= (p | (n -' 1)) ^ <*(p . n)*> by A1, XREAL_1:235 ;
hence p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by RFINSEQ:8; ::_thesis: verum
end;