FINSEQ_3: Non-contiguous Substrings and One-to-one Finite Sequences

:: Non-contiguous Substrings and One-to-one Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem Th1: :: FINSEQ_3:1

Seg 3 = {1,2,3}

proof end;

theorem Th2: :: FINSEQ_3:2

Seg 4 = {1,2,3,4}

proof end;

theorem Th3: :: FINSEQ_3:3

Seg 5 = {1,2,3,4,5}

proof end;

theorem Th4: :: FINSEQ_3:4

Seg 6 = {1,2,3,4,5,6}

proof end;

theorem Th5: :: FINSEQ_3:5

Seg 7 = {1,2,3,4,5,6,7}

proof end;

theorem :: FINSEQ_3:6

Seg 8 = {1,2,3,4,5,6,7,8}

proof end;

theorem Th7: :: FINSEQ_3:7

for k being natural number holds
( Seg k = {} iff not k in Seg k )

proof end;

theorem :: FINSEQ_3:8

canceled;

theorem Th9: :: FINSEQ_3:9

for k being natural number holds not k + 1 in Seg k

proof end;

theorem :: FINSEQ_3:10

for k, n being natural number st k <> 0 holds
k in Seg (k + n)

proof end;

theorem Th11: :: FINSEQ_3:11

for k, n being natural number st k + n in Seg k holds
n = 0

proof end;

theorem :: FINSEQ_3:12

for k, n being natural number st k < n holds
k + 1 in Seg n

proof end;

theorem Th13: :: FINSEQ_3:13

for k, n, m being natural number st k in Seg n & m < k holds
k - m in Seg n

proof end;

theorem :: FINSEQ_3:14

for k, n being natural number holds
( k - n in Seg k iff n < k )

proof end;

theorem Th15: :: FINSEQ_3:15

for k being natural number holds Seg k misses {(k + 1)}

proof end;

theorem :: FINSEQ_3:16

for k being natural number holds (Seg (k + 1)) \ (Seg k) = {(k + 1)}

proof end;

theorem :: FINSEQ_3:17

for k being natural number holds Seg k <> Seg (k + 1) by Th9, FINSEQ_1:6;

theorem :: FINSEQ_3:18

for k, n being natural number st Seg k = Seg (k + n) holds
n = 0 by Th11, FINSEQ_1:5;

theorem Th19: :: FINSEQ_3:19

for k, n being natural number holds Seg k c= Seg (k + n)

proof end;

theorem Th20: :: FINSEQ_3:20

for k, n being natural number holds Seg k, Seg n are_c=-comparable

proof end;

theorem :: FINSEQ_3:21

canceled;

theorem Th22: :: FINSEQ_3:22

for y being set
for k being natural number st Seg k = {y} holds
( k = 1 & y = 1 )

proof end;

theorem :: FINSEQ_3:23

for x, y being set
for k being natural number st Seg k = {x,y} & x <> y holds
( k = 2 & {x,y} = {1,2} )

proof end;

theorem Th24: :: FINSEQ_3:24

for p, q being FinSequence
for x being set st x in dom p holds
x in dom (p ^ q)

proof end;

theorem :: FINSEQ_3:25

for p being FinSequence
for x being set st x in dom p holds
x is Element of NAT ;

theorem Th26: :: FINSEQ_3:26

for p being FinSequence
for x being set st x in dom p holds
x <> 0

proof end;

theorem Th27: :: FINSEQ_3:27

for p being FinSequence
for n being natural number holds
( n in dom p iff ( 1 <= n & n <= len p ) )

proof end;

theorem :: FINSEQ_3:28

for p being FinSequence
for n being natural number holds
( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )

proof end;

theorem Th29: :: FINSEQ_3:29

for x, y being set holds dom <*x,y*> = Seg 2

proof end;

theorem Th30: :: FINSEQ_3:30

for x, y, z being set holds dom <*x,y,z*> = Seg 3

proof end;

theorem Th31: :: FINSEQ_3:31

for p, q being FinSequence holds
( len p = len q iff dom p = dom q )

proof end;

theorem Th32: :: FINSEQ_3:32

for p, q being FinSequence holds
( len p <= len q iff dom p c= dom q )

proof end;

theorem Th33: :: FINSEQ_3:33

for p being FinSequence
for x being set st x in rng p holds
1 in dom p

proof end;

theorem :: FINSEQ_3:34

for p being FinSequence st rng p <> {} holds
1 in dom p

proof end;

theorem :: FINSEQ_3:35

canceled;

theorem :: FINSEQ_3:36

canceled;

theorem :: FINSEQ_3:37

canceled;

theorem :: FINSEQ_3:38

for x, y being set holds {} <> <*x,y*> ;

theorem :: FINSEQ_3:39

for x, y, z being set holds {} <> <*x,y,z*> ;

theorem Th40: :: FINSEQ_3:40

for x, y, z being set holds <*x*> <> <*y,z*>

proof end;

theorem :: FINSEQ_3:41

for u, x, y, z being set holds <*u*> <> <*x,y,z*>

proof end;

theorem :: FINSEQ_3:42

for u, v, x, y, z being set holds <*u,v*> <> <*x,y,z*>

proof end;

theorem Th43: :: FINSEQ_3:43

for r, p, q being FinSequence st len r = (len p) + (len q) & ( for k being Element of NAT st k in dom p holds
r . k = p . k ) & ( for k being Element of NAT st k in dom q holds
r . ((len p) + k) = q . k ) holds
r = p ^ q

proof end;

Lm1: for A being set
for k being natural number st A c= Seg k holds
Sgm A is one-to-one

proof end;

theorem Th44: :: FINSEQ_3:44

for k being natural number
for A being finite set st A c= Seg k holds
len (Sgm A) = card A

proof end;

theorem :: FINSEQ_3:45

for k being natural number
for A being finite set st A c= Seg k holds
dom (Sgm A) = Seg (card A)

proof end;

theorem Th46: :: FINSEQ_3:46

for X being set
for i, k, l, n, m being natural number st X c= Seg i & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l holds
m < n

proof end;

theorem :: FINSEQ_3:47

canceled;

theorem Th48: :: FINSEQ_3:48

for X, Y being set
for i, j being natural number st X c= Seg i & Y c= Seg j holds
( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )

proof end;

theorem Th49: :: FINSEQ_3:49

Sgm {} = {}

proof end;

theorem :: FINSEQ_3:50

for n being natural number st 0 <> n holds
Sgm {n} = <*n*>

proof end;

theorem :: FINSEQ_3:51

for n, m being natural number st 0 < n & n < m holds
Sgm {n,m} = <*n,m*>

proof end;

theorem Th52: :: FINSEQ_3:52

for k being natural number holds len (Sgm (Seg k)) = k

proof end;

Lm2: for k being natural number holds (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k)

proof end;

Lm3: now

let n be natural number ; :: thesis:
assume A1: for k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ; :: thesis:
let k be natural number ; :: thesis:
set X = Sgm (Seg (k + (n + 1)));
set Y = Sgm (Seg (k + 1));
A2: (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)

proof

reconsider p = (Sgm (Seg (k + 1))) | (Seg k) as FinSequence of NAT by FINSEQ_1:23;
A3: len (Sgm (Seg (k + 1))) = k + 1 by Th52;
then A4: dom (Sgm (Seg (k + 1))) = Seg (k + 1) by FINSEQ_1:def 3;
A5: k <= k + 1 by NAT_1:12;
then A6: dom p = Seg k by A3, FINSEQ_1:21;
A7: rng (Sgm (Seg (k + 1))) = Seg (k + 1) by FINSEQ_1:def 13;
A8: (Sgm (Seg (k + 1))) . (k + 1) = k + 1

proof

k + 1 in dom (Sgm (Seg (k + 1))) by A4, FINSEQ_1:6;
then A9: (Sgm (Seg (k + 1))) . (k + 1) in Seg (k + 1) by A7, FUNCT_1:def 5;
then reconsider n = (Sgm (Seg (k + 1))) . (k + 1) as Element of NAT ;
A10: k < k + 1 by XREAL_1:31;
k + 1 in rng (Sgm (Seg (k + 1))) by A7, FINSEQ_1:6;
then consider x being set such that
A11: x in dom (Sgm (Seg (k + 1))) and
A12: (Sgm (Seg (k + 1))) . x = k + 1 by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A11;
assume not (Sgm (Seg (k + 1))) . (k + 1) = k + 1 ; :: thesis:
then not (Sgm (Seg (k + 1))) . (k + 1) in {(k + 1)} by TARSKI:def 1;
then (Sgm (Seg (k + 1))) . (k + 1) in (Seg (k + 1)) \ {(k + 1)} by A9, XBOOLE_0:def 5;
then A13: (Sgm (Seg (k + 1))) . (k + 1) in Seg k by FINSEQ_1:12;

A14: now

assume A15: x = k + 1 ; :: thesis:
n <= k by A13, FINSEQ_1:3;
hence contradiction by A12, A15, XREAL_1:31; :: thesis:

end;

x <= k + 1 by A3, A11, Th27;
then A16: x < k + 1 by A14, XXREAL_0:1;
1 <= x by A11, Th27;
then A17: k + 1 < n by A3, A12, A16, FINSEQ_1:def 13;
n <= k by A13, FINSEQ_1:3;
hence contradiction by A17, A10, XXREAL_0:2; :: thesis:

end;

A18: Sgm (Seg (k + 1)) is one-to-one by Lm1;
rng p = (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}

proof

thus rng p c= (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A19: x in rng p ; :: thesis:

A20: now

assume x in {(k + 1)} ; :: thesis:
then A21: x = k + 1 by TARSKI:def 1;
A22: k < k + 1 by XREAL_1:31;
A23: k + 1 in dom (Sgm (Seg (k + 1))) by A4, FINSEQ_1:6;
A24: Seg k c= Seg (k + 1) by Th19;
consider y being set such that
A25: y in dom p and
A26: p . y = x by A19, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A25;
A27: (Sgm (Seg (k + 1))) . y = p . y by A25, FUNCT_1:70;
y <= k by A6, A25, FINSEQ_1:3;
hence contradiction by A18, A4, A6, A8, A25, A26, A24, A27, A21, A23, A22, FUNCT_1:def 8; :: thesis:

end;

rng p c= rng (Sgm (Seg (k + 1))) by RELAT_1:99;
hence x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} by A8, A19, A20, XBOOLE_0:def 5; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} ; :: thesis:
then x in rng (Sgm (Seg (k + 1))) by XBOOLE_0:def 5;
then consider y being set such that
A29: y in dom (Sgm (Seg (k + 1))) and
A30: (Sgm (Seg (k + 1))) . y = x by FUNCT_1:def 5;

now

assume y in {(k + 1)} ; :: thesis:
then A31: x = k + 1 by A8, A30, TARSKI:def 1;
not x in {(k + 1)} by A8, A28, XBOOLE_0:def 5;
hence contradiction by A31, TARSKI:def 1; :: thesis:

end;

then y in (Seg (k + 1)) \ {(k + 1)} by A4, A29, XBOOLE_0:def 5;
then A32: y in dom p by A6, FINSEQ_1:12;
then p . y = (Sgm (Seg (k + 1))) . y by FUNCT_1:70;
hence x in rng p by A30, A32, FUNCT_1:def 5; :: thesis:

end;

then A33: rng p = Seg k by A7, A8, FINSEQ_1:12;

now

A34: len p = k by A3, A5, FINSEQ_1:21;
let i, j, l, m be natural number ; :: thesis:
assume that
A35: 1 <= i and
A36: i < j and
A37: j <= len p and
A38: l = p . i and
A39: m = p . j ; :: thesis:
i <= len p by A36, A37, XXREAL_0:2;
then i in dom p by A6, A35, A34, FINSEQ_1:3;
then A40: p . i = (Sgm (Seg (k + 1))) . i by FUNCT_1:70;
1 <= j by A35, A36, XXREAL_0:2;
then j in dom p by A6, A37, A34, FINSEQ_1:3;
then A41: p . j = (Sgm (Seg (k + 1))) . j by FUNCT_1:70;
len (Sgm (Seg (k + 1))) = k + 1 by Th52;
then j <= len (Sgm (Seg (k + 1))) by A37, A34, NAT_1:12;
hence l < m by A35, A36, A38, A39, A40, A41, FINSEQ_1:def 13; :: thesis:

end;

hence (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by A33, FINSEQ_1:def 13; :: thesis:

end;

Sgm (Seg (k + (n + 1))) = Sgm (Seg ((k + 1) + n)) ;
then (Sgm (Seg (k + (n + 1)))) | (Seg (k + 1)) = Sgm (Seg (k + 1)) by A1;
then Sgm (Seg k) = (Sgm (Seg (k + (n + 1)))) | ((Seg (k + 1)) /\ (Seg k)) by A2, RELAT_1:100;
hence (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) by FINSEQ_1:9, NAT_1:12; :: thesis:

end;

Lm4: for n, k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)

proof end;

theorem :: FINSEQ_3:53

for k, n being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) by Lm4;

Lm5: now

let k be Nat; :: thesis:
assume A1: Sgm (Seg k) = idseq k ; :: thesis:
A2: len (idseq (k + 1)) = k + 1 by CARD_1:def 13;
then A3: len (Sgm (Seg (k + 1))) = len (idseq (k + 1)) by Th52;
then A4: dom (Sgm (Seg (k + 1))) = Seg (k + 1) by A2, FINSEQ_1:def 3;

now

let j be Nat; :: thesis:
assume A5: j in dom (Sgm (Seg (k + 1))) ; :: thesis:
then A6: j in (Seg k) \/ {(k + 1)} by A4, FINSEQ_1:11;

now

per cases by A6, XBOOLE_0:def 3;

suppose A7: j in Seg k ; :: thesis:

A8: (idseq (k + 1)) . j = j by A4, A5, FUNCT_1:35;
A9: (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;
(Sgm (Seg k)) . j = j by A1, A7, FUNCT_1:35;
hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A7, A8, A9, FUNCT_1:72; :: thesis:

end;

suppose A10: j in {(k + 1)} ; :: thesis:

set Y = Sgm (Seg k);
set X = Sgm (Seg (k + 1));
A11: j = k + 1 by A10, TARSKI:def 1;
then A12: j in Seg (k + 1) by FINSEQ_1:6;

now

rng (Sgm (Seg (k + 1))) = Seg (k + 1) by FINSEQ_1:def 13;
then A13: (Sgm (Seg (k + 1))) . j in Seg (k + 1) by A5, FUNCT_1:def 5;
then reconsider n = (Sgm (Seg (k + 1))) . j as Element of NAT ;
assume (Sgm (Seg (k + 1))) . j <> j ; :: thesis:
then not (Sgm (Seg (k + 1))) . j in {j} by TARSKI:def 1;
then (Sgm (Seg (k + 1))) . j in (Seg (k + 1)) \ {(k + 1)} by A11, A13, XBOOLE_0:def 5;
then A14: (Sgm (Seg (k + 1))) . j in Seg k by FINSEQ_1:12;
A15: Sgm (Seg (k + 1)) is one-to-one by Lm1;
A16: dom (Sgm (Seg (k + 1))) = Seg (k + 1) by A2, A3, FINSEQ_1:def 3;
A17: k < k + 1 by XREAL_1:31;
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;
then A18: (Sgm (Seg (k + 1))) . n = (Sgm (Seg k)) . n by A14, FUNCT_1:72
.= n by A1, A14, FUNCT_1:35 ;
n <= k by A14, FINSEQ_1:3;
hence contradiction by A11, A12, A16, A13, A15, A18, A17, FUNCT_1:def 8; :: thesis:

end;

hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A11, FINSEQ_1:6, FUNCT_1:35; :: thesis:

end;

hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j ; :: thesis:

end;

hence Sgm (Seg (k + 1)) = idseq (k + 1) by A3, FINSEQ_2:10; :: thesis:

end;

theorem Th54: :: FINSEQ_3:54

for k being natural number holds Sgm (Seg k) = idseq k

proof end;

theorem Th55: :: FINSEQ_3:55

for p being FinSequence
for n being natural number holds
( p | (Seg n) = p iff len p <= n )

proof end;

theorem Th56: :: FINSEQ_3:56

for n, k being natural number holds (idseq (n + k)) | (Seg n) = idseq n

proof end;

theorem :: FINSEQ_3:57

for n, m being natural number holds
( (idseq n) | (Seg m) = idseq m iff m <= n )

proof end;

theorem :: FINSEQ_3:58

for n, m being natural number holds
( (idseq n) | (Seg m) = idseq n iff n <= m )

proof end;

theorem Th59: :: FINSEQ_3:59

for p, q being FinSequence
for k, l being natural number st len p = k + l & q = p | (Seg k) holds
len q = k

proof end;

theorem :: FINSEQ_3:60

for p, q being FinSequence
for k, l being natural number st len p = k + l & q = p | (Seg k) holds
dom q = Seg k

proof end;

theorem Th61: :: FINSEQ_3:61

for p, q being FinSequence
for k being natural number st len p = k + 1 & q = p | (Seg k) holds
p = q ^ <*(p . (k + 1))*>

proof end;

theorem :: FINSEQ_3:62

for p being FinSequence
for X being set holds
( p | X is FinSequence iff ex k being Element of NAT st X /\ (dom p) = Seg k )

proof end;

theorem Th63: :: FINSEQ_3:63

for p, q being FinSequence
for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))

proof end;

theorem Th64: :: FINSEQ_3:64

for p, q being FinSequence
for A being set holds p " A c= (p ^ q) " A

proof end;

definition

let p be FinSequence;
let A be set ;
func p - A -> FinSequence equals :: FINSEQ_3:def 1
p * (Sgm ((dom p) \ (p " A)));
coherence

proof end;

end;

:: deftheorem defines - FINSEQ_3:def 1 :

theorem :: FINSEQ_3:65

canceled;

theorem Th66: :: FINSEQ_3:66

for p being FinSequence
for A being set holds len (p - A) = (len p) - (card (p " A))

proof end;

theorem Th67: :: FINSEQ_3:67

for p being FinSequence
for A being set holds len (p - A) <= len p

proof end;

theorem Th68: :: FINSEQ_3:68

for p being FinSequence
for A being set st len (p - A) = len p holds
A misses rng p

proof end;

theorem :: FINSEQ_3:69

for p being FinSequence
for A being set
for n being natural number st n = (len p) - (card (p " A)) holds
dom (p - A) = Seg n

proof end;

theorem :: FINSEQ_3:70

for p being FinSequence
for A being set holds dom (p - A) c= dom p

proof end;

theorem :: FINSEQ_3:71

for p being FinSequence
for A being set st dom (p - A) = dom p holds
A misses rng p

proof end;

theorem Th72: :: FINSEQ_3:72

for p being FinSequence
for A being set holds rng (p - A) = (rng p) \ A

proof end;

theorem :: FINSEQ_3:73

for p being FinSequence
for A being set holds rng (p - A) c= rng p

proof end;

theorem :: FINSEQ_3:74

for p being FinSequence
for A being set st rng (p - A) = rng p holds
A misses rng p

proof end;

theorem Th75: :: FINSEQ_3:75

for p being FinSequence
for A being set holds
( p - A = {} iff rng p c= A )

proof end;

theorem Th76: :: FINSEQ_3:76

for p being FinSequence
for A being set holds
( p - A = p iff A misses rng p )

proof end;

theorem :: FINSEQ_3:77

for p being FinSequence
for x being set holds
( p - {x} = p iff not x in rng p )

proof end;

theorem :: FINSEQ_3:78

for p being FinSequence holds p - {} = p

proof end;

theorem :: FINSEQ_3:79

for p being FinSequence holds p - (rng p) = {} by Th75;

Lm6: for x, A being set holds
( <*x*> - A = <*x*> iff not x in A )

proof end;

Lm7: for x, A being set holds
( <*x*> - A = {} iff x in A )

proof end;

Lm8: for p being FinSequence
for A being set holds (p ^ {}) - A = (p - A) ^ ({} - A)

proof end;

Lm9: for p being FinSequence
for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)

proof end;

Lm10: now

let q be FinSequence; :: thesis:
let x be set ; :: thesis:
assume A1: for p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ; :: thesis:
let p be FinSequence; :: thesis:
let A be set ; :: thesis:
thus (p ^ (q ^ <*x*>)) - A = ((p ^ q) ^ <*x*>) - A by FINSEQ_1:45
.= ((p ^ q) - A) ^ (<*x*> - A) by Lm9
.= ((p - A) ^ (q - A)) ^ (<*x*> - A) by A1
.= (p - A) ^ ((q - A) ^ (<*x*> - A)) by FINSEQ_1:45
.= (p - A) ^ ((q ^ <*x*>) - A) by Lm9 ; :: thesis:

end;

Lm11: for q, p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A)

proof end;

theorem :: FINSEQ_3:80

for p, q being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) by Lm11;

theorem :: FINSEQ_3:81

for A being set holds {} - A = {} ;

theorem :: FINSEQ_3:82

for x, A being set holds
( <*x*> - A = <*x*> iff not x in A ) by Lm6;

theorem :: FINSEQ_3:83

for x, A being set holds
( <*x*> - A = {} iff x in A ) by Lm7;

theorem Th84: :: FINSEQ_3:84

for x, y, A being set holds
( <*x,y*> - A = {} iff ( x in A & y in A ) )

proof end;

theorem Th85: :: FINSEQ_3:85

for x, A, y being set st x in A & not y in A holds
<*x,y*> - A = <*y*>

proof end;

theorem :: FINSEQ_3:86

for x, y, A being set st <*x,y*> - A = <*y*> & x <> y holds
( x in A & not y in A )

proof end;

theorem Th87: :: FINSEQ_3:87

for x, A, y being set st not x in A & y in A holds
<*x,y*> - A = <*x*>

proof end;

theorem :: FINSEQ_3:88

for x, y, A being set st <*x,y*> - A = <*x*> & x <> y holds
( not x in A & y in A )

proof end;

theorem :: FINSEQ_3:89

for x, y, A being set holds
( <*x,y*> - A = <*x,y*> iff ( not x in A & not y in A ) )

proof end;

theorem Th90: :: FINSEQ_3:90

for p, q being FinSequence
for A being set
for k being natural number st len p = k + 1 & q = p | (Seg k) holds
( p . (k + 1) in A iff p - A = q - A )

proof end;

theorem Th91: :: FINSEQ_3:91

for p, q being FinSequence
for A being set
for k being natural number st len p = k + 1 & q = p | (Seg k) holds
( not p . (k + 1) in A iff p - A = (q - A) ^ <*(p . (k + 1))*> )

proof end;

Lm12: for l being natural number st ( for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ) holds
for p being FinSequence
for A being set st len p = l + 1 holds
for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )

proof end;

Lm13: for l being natural number
for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )

proof end;

theorem :: FINSEQ_3:92

for p being FinSequence
for A being set
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )

proof end;

theorem :: FINSEQ_3:93

for p being FinSequence
for D, A being set st p is FinSequence of D holds
p - A is FinSequence of D

proof end;

theorem :: FINSEQ_3:94

for p being FinSequence
for A being set st p is one-to-one holds
p - A is one-to-one

proof end;

theorem Th95: :: FINSEQ_3:95

for p being FinSequence
for A being set st p is one-to-one holds
len (p - A) = (len p) - (card (A /\ (rng p)))

proof end;

theorem Th96: :: FINSEQ_3:96

for p being FinSequence
for A being finite set st p is one-to-one & A c= rng p holds
len (p - A) = (len p) - (card A)

proof end;

theorem :: FINSEQ_3:97

for p being FinSequence
for x being set st p is one-to-one & x in rng p holds
len (p - {x}) = (len p) - 1

proof end;

theorem Th98: :: FINSEQ_3:98

for p, q being FinSequence holds
( ( rng p misses rng q & p is one-to-one & q is one-to-one ) iff p ^ q is one-to-one )

proof end;

theorem :: FINSEQ_3:99

for A being set
for k being natural number st A c= Seg k holds
Sgm A is one-to-one by Lm1;

theorem :: FINSEQ_3:100

canceled;

theorem :: FINSEQ_3:101

canceled;

theorem Th102: :: FINSEQ_3:102

for x being set holds <*x*> is one-to-one

proof end;

theorem Th103: :: FINSEQ_3:103

for x, y being set holds
( x <> y iff <*x,y*> is one-to-one )

proof end;

theorem Th104: :: FINSEQ_3:104

for x, y, z being set holds
( ( x <> y & y <> z & z <> x ) iff <*x,y,z*> is one-to-one )

proof end;

theorem Th105: :: FINSEQ_3:105

for p being FinSequence
for x being set st p is one-to-one & rng p = {x} holds
len p = 1

proof end;

theorem :: FINSEQ_3:106

for p being FinSequence
for x being set st p is one-to-one & rng p = {x} holds
p = <*x*>

proof end;

theorem Th107: :: FINSEQ_3:107

for p being FinSequence
for x, y being set st p is one-to-one & rng p = {x,y} & x <> y holds
len p = 2

proof end;

theorem :: FINSEQ_3:108

for p being FinSequence
for x, y being set st p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> holds
p = <*y,x*>

proof end;

theorem Th109: :: FINSEQ_3:109

for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one holds
len p = 3

proof end;

theorem :: FINSEQ_3:110

for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z holds
len p = 3

proof end;

begin

theorem :: FINSEQ_3:111

for D being non empty set
for df being FinSequence of D st not df is empty holds
ex d being Element of D ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 )

proof end;

theorem :: FINSEQ_3:112

for i being natural number
for df being FinSequence
for d being set st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i

proof end;

definition

let i be natural number ;
let p be FinSequence;
func Del (p,i) -> FinSequence equals :: FINSEQ_3:def 2
p * (Sgm ((dom p) \ {i}));
coherence

proof end;

end;

:: deftheorem defines Del FINSEQ_3:def 2 :

theorem Th113: :: FINSEQ_3:113

for i being natural number
for p being FinSequence holds
( ( i in dom p implies ex m being Nat st
( len p = m + 1 & len (Del (p,i)) = m ) ) & ( not i in dom p implies Del (p,i) = p ) )

proof end;

theorem :: FINSEQ_3:114

for i being natural number
for D being non empty set
for p being FinSequence of D holds Del (p,i) is FinSequence of D

proof end;

theorem :: FINSEQ_3:115

for i being natural number
for p being FinSequence holds rng (Del (p,i)) c= rng p

proof end;

theorem Th116: :: FINSEQ_3:116

for n, m, i being natural number st n = m + 1 & i in Seg n holds
len (Sgm ((Seg n) \ {i})) = m

proof end;

theorem Th117: :: FINSEQ_3:117

for i, k, m, n being Nat st n = m + 1 & k in Seg n & i in Seg m holds
( ( 1 <= i & i < k implies (Sgm ((Seg n) \ {k})) . i = i ) & ( k <= i & i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) )

proof end;

theorem Th118: :: FINSEQ_3:118

for m, n being natural number
for f being FinSequence st len f = m + 1 & n in dom f holds
len (Del (f,n)) = m

proof end;

theorem :: FINSEQ_3:119

for k, n being natural number
for f being FinSequence st k < n holds
(Del (f,n)) . k = f . k

proof end;

theorem :: FINSEQ_3:120

for m, n, k being natural number
for f being FinSequence st len f = m + 1 & n in dom f & n <= k & k <= m holds
(Del (f,n)) . k = f . (k + 1)

proof end;

theorem Th121: :: FINSEQ_3:121

for k, n being natural number
for f being FinSequence st k <= n holds
(f | n) . k = f . k

proof end;

theorem :: FINSEQ_3:122

for p, q being FinSequence st p c= q holds
q | (len p) = p

proof end;

theorem Th123: :: FINSEQ_3:123

for A being set
for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)

proof end;

theorem :: FINSEQ_3:124

for F being FinSequence
for A being Subset of (rng F) ex p being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * p

proof end;

theorem :: FINSEQ_3:125

for f being FinSubsequence st f is FinSequence holds
Seq f = f

proof end;

theorem :: FINSEQ_3:126

for t being FinSequence of INT holds t is FinSequence of REAL

proof end;

theorem :: FINSEQ_3:127

for p, q being FinSequence holds
( len p < len q iff dom p c< dom q )

proof end;

theorem Th128: :: FINSEQ_3:128

for A being set
for i being Nat holds
( ( i <> 0 & A = {} ) iff i -tuples_on A = {} )

proof end;

registration

let i be Nat;
let D be set ;
cluster i -tuples_on D -> with_common_domain ;
coherence

proof end;

end;

registration

let i be Nat;
let D be set ;
cluster i -tuples_on D -> product-like ;
coherence

proof end;

end;

begin

theorem :: FINSEQ_3:129

for D1, D2 being non empty set
for p being FinSequence of D1
for f being Function of D1,D2 holds
( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )

proof end;

definition

let D be non empty set ;
let R be Relation of D;
func ExtendRel R -> Relation of (D *) means :Def3: :: FINSEQ_3:def 3
for x, y being FinSequence of D holds
( [x,y] in it iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ExtendRel FINSEQ_3:def 3 :

theorem :: FINSEQ_3:130

for D being non empty set holds ExtendRel (id D) = id (D *)

proof end;

definition

let D be non empty set ;
let R be Equivalence_Relation of D;
let y be FinSequence of Class R;
let x be FinSequence of D;
pred x is_representatives_FS y means :: FINSEQ_3:def 4
( len x = len y & ( for n being Element of NAT st n in dom x holds
Class (R,(x . n)) = y . n ) );

end;

:: deftheorem defines is_representatives_FS FINSEQ_3:def 4 :

theorem :: FINSEQ_3:131

for D being non empty set
for R being Equivalence_Relation of D
for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y

proof end;