:: by Czes\law Byli\'nski

::

:: Received January 25, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

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 )

for x, y being set st f " {y} = {x} holds

( x in dom f & y in rng f & f . x = y )

proof 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} )

( f is one-to-one iff for x being set st x in dom f holds

f " {(f . x)} = {x} )

proof 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

for y1, y2 being set st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds

y1 = y2

proof end;

registration

let x be set ;

coherence

<*x*> is trivial ;

let y be set ;

coherence

not <*x,y*> is trivial

end;
coherence

<*x*> is trivial ;

let y be set ;

coherence

not <*x,y*> is trivial

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is one-to-one & not b_{1} is empty )
end;

cluster non empty Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof 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))*>

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

registration

let D be non empty set ;

ex b_{1} being FinSequence of D st

( b_{1} is one-to-one & not b_{1} is empty )

end;
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 b

( b

proof end;

:: FINSEQ_1:17

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

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

:: FINSEQ_1:18

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

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

for p being Element of D

for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p

proof 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 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))*>

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

registration

let i be Nat;

let D be non empty set ;

let f be one-to-one FinSequence of D;

coherence

f | i is one-to-one by Lm2;

end;
let D be non empty set ;

let f be one-to-one FinSequence of D;

coherence

f | i is one-to-one by Lm2;

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

for D being set

for f, g being FinSequence of D st i <= len f holds

(f ^ g) | i = f | i

proof 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)

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

for D being set

for f being FinSequence of D st i in dom (f /^ n) holds

n + i in dom f

proof 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)

for D being set

for f being FinSequence of D st i in dom (f /^ n) holds

(f /^ n) /. i = f /. (n + i)

proof 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)

for f being FinSequence of D st not f is empty holds

f = <*(f /. 1)*> ^ (f /^ 1)

proof 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))*>

for D being non empty set

for f being FinSequence of D st i + 1 = len f holds

f /^ i = <*(f /. (len f))*>

proof 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

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

registration

let i be Nat;

let D be non empty set ;

let f be one-to-one FinSequence of D;

coherence

f /^ i is one-to-one by Lm3;

end;
let D be non empty set ;

let f be one-to-one FinSequence of D;

coherence

f /^ i is one-to-one by Lm3;

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)

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 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)

for p being Element of D

for f being FinSequence of D st p in rng f holds

f |-- p = f /^ (p .. f)

proof 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

for D being non empty set

for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i

proof 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

for p being Element of D

for f being FinSequence of D st p in rng f holds

f /. (p .. f) = p

proof 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

for D being non empty set

for f being FinSequence of D st i in dom f holds

(f /. i) .. f <= i

proof 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

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

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

definition

let D be non empty set ;

let f be FinSequence of D;

let p be set ;

correctness

coherence

f | (p .. f) is FinSequence of D;

;

end;
let f be FinSequence of D;

let p be set ;

correctness

coherence

f | (p .. f) is FinSequence of D;

;

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

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

for p being Element of D

for f being FinSequence of D st p in rng f holds

len (f -: p) = p .. f

proof 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

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

for p being Element of D

for f being FinSequence of D st p in rng f holds

(f -: p) /. 1 = f /. 1

proof 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

for p being Element of D

for f being FinSequence of D st p in rng f holds

(f -: p) /. (p .. f) = p

proof 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)

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

for p being Element of D

for f being FinSequence of D st p in rng f holds

not f -: p is empty

proof end;

theorem :: FINSEQ_5:48

registration

let D be non empty set ;

let p be Element of D;

let f be one-to-one FinSequence of D;

coherence

f -: p is one-to-one ;

end;
let p be Element of D;

let f be one-to-one FinSequence of D;

coherence

f -: p is one-to-one ;

definition

let D be non empty set ;

let f be FinSequence of D;

let p be Element of D;

coherence

<*p*> ^ (f /^ (p .. f)) is FinSequence of D ;

end;
let f be FinSequence of D;

let p be Element of D;

coherence

<*p*> ^ (f /^ (p .. f)) is FinSequence of D ;

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

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 )

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

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

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

registration

let D be non empty set ;

let p be Element of D;

let f be FinSequence of D;

coherence

not f :- p is empty ;

end;
let p be Element of D;

let f be FinSequence of D;

coherence

not f :- p is empty ;

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))

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

theorem :: FINSEQ_5:53

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)

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

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

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

definition

let f be FinSequence;

ex b_{1} being FinSequence st

( len b_{1} = len f & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = f . (((len f) - i) + 1) ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = len f & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = f . (((len f) - i) + 1) ) & len b_{2} = len f & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = f . (((len f) - i) + 1) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being FinSequence st len b_{1} = len b_{2} & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = b_{2} . (((len b_{2}) - i) + 1) ) holds

( len b_{2} = len b_{1} & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = b_{1} . (((len b_{1}) - i) + 1) ) )

end;
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 ( len it = len f & ( for i being Nat st i in dom it holds

it . i = f . (((len f) - i) + 1) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

( len b

b

proof end;

:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :

for f, b_{2} being FinSequence holds

( b_{2} = Rev f iff ( len b_{2} = len f & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = f . (((len f) - i) + 1) ) ) );

for f, b

( b

b

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)

for i, j being Nat st i in dom f & i + j = (len f) + 1 holds

j in dom (Rev f)

proof end;

registration
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

end;
let f be FinSequence of D;

:: original: Rev

redefine func Rev f -> FinSequence of D;

coherence

Rev f is FinSequence of D

proof 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 )

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

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

definition

let D be non empty set ;

let f be FinSequence of D;

let p be Element of D;

let n be Nat;

correctness

coherence

((f | n) ^ <*p*>) ^ (f /^ n) is FinSequence of D;

;

end;
let f be FinSequence of D;

let p be Element of D;

let n be Nat;

correctness

coherence

((f | n) ^ <*p*>) ^ (f /^ n) is FinSequence of D;

;

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

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

for p being Element of D

for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f

proof 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*>

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

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 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)

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

registration

let D be non empty set ;

let f be FinSequence of D;

let n be Nat;

let p be Element of D;

coherence

not Ins (f,n,p) is empty ;

end;
let f be FinSequence of D;

let n be Nat;

let p be Element of D;

coherence

not Ins (f,n,p) is empty ;

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))

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

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

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

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

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

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

begin

:: from JORDAN4, 2005.11.16, A.T.

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 )

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

:: from AMISTD_1, 2006.03,15, A.T.

registration

not for b_{1} being FinSequence holds b_{1} is trivial
end;

cluster non trivial Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like for set ;

existence not for b

proof end;

:: from JORDAN3, 2007.03.09, A.T

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

for f being FinSequence of D

for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

proof 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))*>

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

:: from JORDAN3, 2007.03.18, A.T.

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))*>

for p being FinSequence of D

for i being Nat st i < len p holds

p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>

proof end;

:: from POLYNOM4, 2007.03.18, A.T.

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)

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