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


begin

theorem Th1: :: FINSEQ_3:1
Seg 3 = {1,2,3}
proofend;

theorem Th2: :: FINSEQ_3:2
Seg 4 = {1,2,3,4}
proofend;

theorem Th3: :: FINSEQ_3:3
Seg 5 = {1,2,3,4,5}
proofend;

theorem Th4: :: FINSEQ_3:4
Seg 6 = {1,2,3,4,5,6}
proofend;

theorem Th5: :: FINSEQ_3:5
Seg 7 = {1,2,3,4,5,6,7}
proofend;

theorem :: FINSEQ_3:6
Seg 8 = {1,2,3,4,5,6,7,8}
proofend;

theorem Th7: :: FINSEQ_3:7
for k being Nat holds
( Seg k = {} iff not k in Seg k )
proofend;

theorem Th8: :: FINSEQ_3:8
for k being Nat holds not k + 1 in Seg k
proofend;

theorem :: FINSEQ_3:9
for k, n being Nat st k <> 0 holds
k in Seg (k + n)
proofend;

theorem Th10: :: FINSEQ_3:10
for k, n being Nat st k + n in Seg k holds
n = 0
proofend;

theorem :: FINSEQ_3:11
for k, n being Nat st k < n holds
k + 1 in Seg n
proofend;

theorem Th12: :: FINSEQ_3:12
for k, n, m being Nat st k in Seg n &amp; m < k holds
k - m in Seg n
proofend;

theorem :: FINSEQ_3:13
for k, n being Nat holds
( k - n in Seg k iff n < k )
proofend;

theorem Th14: :: FINSEQ_3:14
for k being Nat holds Seg k misses {(k + 1)}
proofend;

theorem :: FINSEQ_3:15
for k being Nat holds (Seg (k + 1)) \ (Seg k) = {(k + 1)}
proofend;

:: Theorem Seg(k + 1) \ {k + 1} = Seg k is
:: proved in RLVECT_1 and has a number 104.
theorem :: FINSEQ_3:16
for k being Nat holds Seg k <> Seg (k + 1) by Th8, FINSEQ_1:4;

theorem :: FINSEQ_3:17
for k, n being Nat st Seg k = Seg (k + n) holds
n = 0 by Th10, FINSEQ_1:3;

theorem Th18: :: FINSEQ_3:18
for k, n being Nat holds Seg k c= Seg (k + n)
proofend;

theorem Th19: :: FINSEQ_3:19
for k, n being Nat holds Seg k, Seg n are_c=-comparable
proofend;

theorem Th20: :: FINSEQ_3:20
for y being set
for k being Nat st Seg k = {y} holds
( k = 1 &amp; y = 1 )
proofend;

theorem :: FINSEQ_3:21
for x, y being set
for k being Nat st Seg k = {x,y} &amp; x <> y holds
( k = 2 &amp; {x,y} = {1,2} )
proofend;

theorem Th22: :: FINSEQ_3:22
for p, q being FinSequence
for x being set st x in dom p holds
x in dom (p ^ q)
proofend;

theorem :: FINSEQ_3:23
for p being FinSequence
for x being set st x in dom p holds
x is Element of NAT ;

theorem Th24: :: FINSEQ_3:24
for p being FinSequence
for x being set st x in dom p holds
x <> 0
proofend;

theorem Th25: :: FINSEQ_3:25
for p being FinSequence
for n being Nat holds
( n in dom p iff ( 1 <= n &amp; n <= len p ) )
proofend;

theorem :: FINSEQ_3:26
for p being FinSequence
for n being Nat holds
( n in dom p iff ( n - 1 is Element of NAT &amp; (len p) - n is Element of NAT ) )
proofend;

theorem :: FINSEQ_3:27
canceled;

theorem :: FINSEQ_3:28
canceled;

theorem Th29: :: FINSEQ_3:29
for p, q being FinSequence holds
( len p = len q iff dom p = dom q )
proofend;

theorem Th30: :: FINSEQ_3:30
for p, q being FinSequence holds
( len p <= len q iff dom p c= dom q )
proofend;

theorem Th31: :: FINSEQ_3:31
for p being FinSequence
for x being set st x in rng p holds
1 in dom p
proofend;

theorem :: FINSEQ_3:32
for p being FinSequence st rng p <> {} holds
1 in dom p
proofend;

theorem :: FINSEQ_3:33
for x, y being set holds {} <> <*x,y*> ;

theorem :: FINSEQ_3:34
for x, y, z being set holds {} <> <*x,y,z*> ;

theorem Th35: :: FINSEQ_3:35
for x, y, z being set holds <*x*> <> <*y,z*>
proofend;

theorem :: FINSEQ_3:36
for u, x, y, z being set holds <*u*> <> <*x,y,z*>
proofend;

theorem :: FINSEQ_3:37
for u, v, x, y, z being set holds <*u,v*> <> <*x,y,z*>
proofend;

theorem Th38: :: FINSEQ_3:38
for r, p, q being FinSequence st len r = (len p) + (len q) &amp; ( for k being Element of NAT st k in dom p holds
r . k = p . k ) &amp; ( for k being Element of NAT st k in dom q holds
r . ((len p) + k) = q . k ) holds
r = p ^ q
proofend;

Lm1:  for A being set
for k being Nat st A c= Seg k holds
Sgm A is one-to-one
proofend;

theorem Th39: :: FINSEQ_3:39
for k being Nat
for A being finite set st A c= Seg k holds
len (Sgm A) = card A
proofend;

theorem :: FINSEQ_3:40
for k being Nat
for A being finite set st A c= Seg k holds
dom (Sgm A) = Seg (card A)
proofend;

theorem Th41: :: FINSEQ_3:41
for X being set
for i, k, l, n, m being Nat st X c= Seg i &amp; k < l &amp; 1 <= n &amp; m <= len (Sgm X) &amp; (Sgm X) . m = k &amp; (Sgm X) . n = l holds
m < n
proofend;

theorem Th42: :: FINSEQ_3:42
for X, Y being set
for i, j being Nat st X c= Seg i &amp; Y c= Seg j holds
( ( for m, n being Element of NAT st m in X &amp; n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
proofend;

theorem Th43: :: FINSEQ_3:43
Sgm {} = {}
proofend;

:: The other way of the one above - FINSEQ_1:72.
theorem :: FINSEQ_3:44
for n being Nat st 0 <> n holds
Sgm {n} = <*n*>
proofend;

theorem :: FINSEQ_3:45
for n, m being Nat st 0 < n &amp; n < m holds
Sgm {n,m} = <*n,m*>
proofend;

theorem Th46: :: FINSEQ_3:46
for k being Nat holds len (Sgm (Seg k)) = k
proofend;

Lm2:  for k being Nat holds (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k)
proofend;

Lm3: now__::_thesis:_for_n_being_Nat_st_(_for_k_being_Nat_holds_(Sgm_(Seg_(k_+_n)))_|_(Seg_k)_=_Sgm_(Seg_k)_)_holds_
for_k_being_Nat_holds_(Sgm_(Seg_(k_+_(n_+_1))))_|_(Seg_k)_=_Sgm_(Seg_k)
let n be Nat; ::_thesis: ( ( for k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ) implies for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) )
assume A1: for k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ; ::_thesis: for k being Nat holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
let k be Nat; ::_thesis: (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
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:18;
A3: len (Sgm (Seg (k + 1))) = k + 1 by Th46;
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:17;
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:4;
then A9: (Sgm (Seg (k + 1))) . (k + 1) in Seg (k + 1) by A7, FUNCT_1:def_3;
then reconsider n = (Sgm (Seg (k + 1))) . (k + 1) as Element of NAT ;
A10: k < k + 1 by XREAL_1:29;
 k + 1 in rng (Sgm (Seg (k + 1))) by A7, FINSEQ_1:4;
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_3;
reconsider x = x as Element of NAT by A11;
assume  not (Sgm (Seg (k + 1))) . (k + 1) = k + 1 ; ::_thesis: contradiction
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:10;
A14: now__::_thesis:_not_x_=_k_+_1
assume A15: x = k + 1 ; ::_thesis: contradiction
 n <= k by A13, FINSEQ_1:1;
hence  contradiction by A12, A15, XREAL_1:29; ::_thesis: verum
end;
 x <= k + 1 by A3, A11, Th25;
then A16: x < k + 1 by A14, XXREAL_0:1;
 1 <= x by A11, Th25;
then A17: k + 1 < n by A3, A12, A16, FINSEQ_1:def_13;
 n <= k by A13, FINSEQ_1:1;
hence  contradiction by A17, A10, XXREAL_0:2; ::_thesis: verum
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 toXBOOLE_0:def_10 ::_thesis: (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} c= rng p
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in rng p or x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} )
assume A19: x in rng p ; ::_thesis: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
A20: now__::_thesis:_not_x_in_{(k_+_1)}
assume  x in {(k + 1)} ; ::_thesis: contradiction
then A21: x = k + 1 by TARSKI:def_1;
A22: k < k + 1 by XREAL_1:29;
A23: k + 1 in dom (Sgm (Seg (k + 1))) by A4, FINSEQ_1:4;
A24: Seg k c= Seg (k + 1) by Th18;
consider y being set  such that
A25: y in dom p and
A26: p . y = x by A19, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A25;
A27: (Sgm (Seg (k + 1))) . y = p . y by A25, FUNCT_1:47;
 y <= k by A6, A25, FINSEQ_1:1;
hence  contradiction by A18, A4, A6, A8, A25, A26, A24, A27, A21, A23, A22, FUNCT_1:def_4; ::_thesis: verum
end;
 rng p c= rng (Sgm (Seg (k + 1))) by RELAT_1:70;
hence  x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} by A8, A19, A20, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} or x in rng p )
assume A28: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} ; ::_thesis: x in rng p
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_3;
now__::_thesis:_not_y_in_{(k_+_1)}
assume  y in {(k + 1)} ; ::_thesis: contradiction
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: verum
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:10;
then  p . y = (Sgm (Seg (k + 1))) . y by FUNCT_1:47;
hence  x in rng p by A30, A32, FUNCT_1:def_3; ::_thesis: verum
end;
then A33: rng p = Seg k by A7, A8, FINSEQ_1:10;
now__::_thesis:_for_i,_j,_l,_m_being_Nat_st_1_<=_i_&amp;_i_<_j_&amp;_j_<=_len_p_&amp;_l_=_p_._i_&amp;_m_=_p_._j_holds_
l_<_m
A34: len p = k by A3, A5, FINSEQ_1:17;
let i, j, l, m be Nat; ::_thesis: ( 1 <= i &amp; i < j &amp; j <= len p &amp; l = p . i &amp; m = p . j implies l < m )
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: l < m
 i <= len p by A36, A37, XXREAL_0:2;
then  i in dom p by A6, A35, A34, FINSEQ_1:1;
then A40: p . i = (Sgm (Seg (k + 1))) . i by FUNCT_1:47;
 1 <= j by A35, A36, XXREAL_0:2;
then  j in dom p by A6, A37, A34, FINSEQ_1:1;
then A41: p . j = (Sgm (Seg (k + 1))) . j by FUNCT_1:47;
 len (Sgm (Seg (k + 1))) = k + 1 by Th46;
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: verum
end;
hence  (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by A33, FINSEQ_1:def_13; ::_thesis: verum
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:71;
hence  (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) by FINSEQ_1:7, NAT_1:12; ::_thesis: verum
end;

Lm4:  for n, k being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)
proofend;

theorem :: FINSEQ_3:47
for k, n being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) by Lm4;

Lm5: now__::_thesis:_for_k_being_Nat_st_Sgm_(Seg_k)_=_idseq_k_holds_
Sgm_(Seg_(k_+_1))_=_idseq_(k_+_1)
let k be Nat; ::_thesis: ( Sgm (Seg k) = idseq k implies Sgm (Seg (k + 1)) = idseq (k + 1) )
assume A1: Sgm (Seg k) = idseq k ; ::_thesis: Sgm (Seg (k + 1)) = idseq (k + 1)
A2: len (idseq (k + 1)) = k + 1 by CARD_1:def_7;
then A3: len (Sgm (Seg (k + 1))) = len (idseq (k + 1)) by Th46;
then A4: dom (Sgm (Seg (k + 1))) = Seg (k + 1) by A2, FINSEQ_1:def_3;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Sgm_(Seg_(k_+_1)))_holds_
(Sgm_(Seg_(k_+_1)))_._j_=_(idseq_(k_+_1))_._j
let j be Nat; ::_thesis: ( j in dom (Sgm (Seg (k + 1))) implies (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j )
assume A5: j in dom (Sgm (Seg (k + 1))) ; ::_thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
then A6: j in (Seg k) \/ {(k + 1)} by A4, FINSEQ_1:9;
now__::_thesis:_(Sgm_(Seg_(k_+_1)))_._j_=_(idseq_(k_+_1))_._j
percases ( j in Seg k or j in {(k + 1)} ) by A6, XBOOLE_0:def_3;
supposeA7: j in Seg k ; ::_thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
A8: (idseq (k + 1)) . j = j by A4, A5, FUNCT_1:18;
A9: (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;
 (Sgm (Seg k)) . j = j by A1, A7, FUNCT_1:18;
hence  (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A7, A8, A9, FUNCT_1:49; ::_thesis: verum
end;
supposeA10: j in {(k + 1)} ; ::_thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
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:4;
now__::_thesis:_not_(Sgm_(Seg_(k_+_1)))_._j_<>_j
 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_3;
then reconsider n = (Sgm (Seg (k + 1))) . j as Element of NAT ;
assume  (Sgm (Seg (k + 1))) . j <> j ; ::_thesis: contradiction
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:10;
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:29;
 (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:49
.= n by A1, A14, FUNCT_1:18 ;
 n <= k by A14, FINSEQ_1:1;
hence  contradiction by A11, A12, A16, A13, A15, A18, A17, FUNCT_1:def_4; ::_thesis: verum
end;
hence  (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A11, FINSEQ_1:4, FUNCT_1:18; ::_thesis: verum
end;
end;
end;
hence  (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j ; ::_thesis: verum
end;
hence  Sgm (Seg (k + 1)) = idseq (k + 1) by A3, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th48: :: FINSEQ_3:48
for k being Nat holds Sgm (Seg k) = idseq k
proofend;

theorem Th49: :: FINSEQ_3:49
for p being FinSequence
for n being Nat holds
( p | (Seg n) = p iff len p <= n )
proofend;

theorem Th50: :: FINSEQ_3:50
for n, k being Nat holds (idseq (n + k)) | (Seg n) = idseq n
proofend;

theorem :: FINSEQ_3:51
for n, m being Nat holds
( (idseq n) | (Seg m) = idseq m iff m <= n )
proofend;

theorem :: FINSEQ_3:52
for n, m being Nat holds
( (idseq n) | (Seg m) = idseq n iff n <= m )
proofend;

theorem Th53: :: FINSEQ_3:53
for p, q being FinSequence
for k, l being Nat st len p = k + l &amp; q = p | (Seg k) holds
len q = k
proofend;

theorem :: FINSEQ_3:54
for p, q being FinSequence
for k, l being Nat st len p = k + l &amp; q = p | (Seg k) holds
dom q = Seg k
proofend;

theorem Th55: :: FINSEQ_3:55
for p, q being FinSequence
for k being Nat st len p = k + 1 &amp; q = p | (Seg k) holds
p = q ^ <*(p . (k + 1))*>
proofend;

theorem :: FINSEQ_3:56
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 )
proofend;

theorem Th57: :: FINSEQ_3:57
for p, q being FinSequence
for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))
proofend;

theorem Th58: :: FINSEQ_3:58
for p, q being FinSequence
for A being set holds p " A c= (p ^ q) " A
proofend;

definition
let p be FinSequence;
let A be set ;
funcp - A ->  FinSequence equals :: FINSEQ_3:def 1
p * (Sgm ((dom p) \ (p " A)));
coherence
 p * (Sgm ((dom p) \ (p " A))) is FinSequence
proofend;
end;

:: deftheorem  defines - FINSEQ_3:def_1_:_
 for p being FinSequence
for A being set holds p - A = p * (Sgm ((dom p) \ (p " A)));

theorem Th59: :: FINSEQ_3:59
for p being FinSequence
for A being set holds len (p - A) = (len p) - (card (p " A))
proofend;

theorem Th60: :: FINSEQ_3:60
for p being FinSequence
for A being set holds len (p - A) <= len p
proofend;

theorem Th61: :: FINSEQ_3:61
for p being FinSequence
for A being set st len (p - A) = len p holds
A misses rng p
proofend;

theorem :: FINSEQ_3:62
for p being FinSequence
for A being set
for n being Nat st n = (len p) - (card (p " A)) holds
dom (p - A) = Seg n
proofend;

theorem :: FINSEQ_3:63
for p being FinSequence
for A being set holds dom (p - A) c= dom p
proofend;

theorem :: FINSEQ_3:64
for p being FinSequence
for A being set st dom (p - A) = dom p holds
A misses rng p
proofend;

theorem Th65: :: FINSEQ_3:65
for p being FinSequence
for A being set holds rng (p - A) = (rng p) \ A
proofend;

theorem :: FINSEQ_3:66
for p being FinSequence
for A being set holds rng (p - A) c= rng p
proofend;

theorem :: FINSEQ_3:67
for p being FinSequence
for A being set st rng (p - A) = rng p holds
A misses rng p
proofend;

theorem Th68: :: FINSEQ_3:68
for p being FinSequence
for A being set holds
( p - A = {} iff rng p c= A )
proofend;

theorem Th69: :: FINSEQ_3:69
for p being FinSequence
for A being set holds
( p - A = p iff A misses rng p )
proofend;

theorem :: FINSEQ_3:70
for p being FinSequence
for x being set holds
( p - {x} = p iff not x in rng p )
proofend;

theorem :: FINSEQ_3:71
for p being FinSequence holds p - {} = p
proofend;

theorem :: FINSEQ_3:72
for p being FinSequence holds p - (rng p) = {} by Th68;

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

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

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

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

Lm10: now__::_thesis:_for_q_being_FinSequence
for_x_being_set_st_(_for_p_being_FinSequence
for_A_being_set_holds_(p_^_q)_-_A_=_(p_-_A)_^_(q_-_A)_)_holds_
for_p_being_FinSequence
for_A_being_set_holds_(p_^_(q_^_<*x*>))_-_A_=_(p_-_A)_^_((q_^_<*x*>)_-_A)
let q be FinSequence; ::_thesis: for x being set st ( for p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) holds
for p being FinSequence
for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)
let x be set ; ::_thesis: ( ( for p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ) implies for p being FinSequence
for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A) )
assume A1: for p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ; ::_thesis: for p being FinSequence
for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)
let p be FinSequence; ::_thesis: for A being set holds (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)
let A be set ; ::_thesis: (p ^ (q ^ <*x*>)) - A = (p - A) ^ ((q ^ <*x*>) - A)
thus (p ^ (q ^ <*x*>)) - A = ((p ^ q) ^ <*x*>) - A by FINSEQ_1:32
.= ((p ^ q) - A) ^ (<*x*> - A) by Lm9
.= ((p - A) ^ (q - A)) ^ (<*x*> - A) by A1
.= (p - A) ^ ((q - A) ^ (<*x*> - A)) by FINSEQ_1:32
.= (p - A) ^ ((q ^ <*x*>) - A) by Lm9 ; ::_thesis: verum
end;

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

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

theorem :: FINSEQ_3:74
for A being set holds {} - A = {} ;

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

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

theorem Th77: :: FINSEQ_3:77
for x, y, A being set holds
( <*x,y*> - A = {} iff ( x in A &amp; y in A ) )
proofend;

theorem Th78: :: FINSEQ_3:78
for x, A, y being set st x in A &amp; not y in A holds
<*x,y*> - A = <*y*>
proofend;

theorem :: FINSEQ_3:79
for x, y, A being set st <*x,y*> - A = <*y*> &amp; x <> y holds
( x in A &amp; not y in A )
proofend;

theorem Th80: :: FINSEQ_3:80
for x, A, y being set st not x in A &amp; y in A holds
<*x,y*> - A = <*x*>
proofend;

theorem :: FINSEQ_3:81
for x, y, A being set st <*x,y*> - A = <*x*> &amp; x <> y holds
( not x in A &amp; y in A )
proofend;

theorem :: FINSEQ_3:82
for x, y, A being set holds
( <*x,y*> - A = <*x,y*> iff ( not x in A &amp; not y in A ) )
proofend;

theorem Th83: :: FINSEQ_3:83
for p, q being FinSequence
for A being set
for k being Nat st len p = k + 1 &amp; q = p | (Seg k) holds
( p . (k + 1) in A iff p - A = q - A )
proofend;

theorem Th84: :: FINSEQ_3:84
for p, q being FinSequence
for A being set
for k being Nat st len p = k + 1 &amp; q = p | (Seg k) holds
( not p . (k + 1) in A iff p - A = (q - A) ^ <*(p . (k + 1))*> )
proofend;

Lm12:  for l being Nat st ( for p being FinSequence
for A being set st len p = l holds
for n being Nat 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 &amp; k <= n &amp; 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 Nat 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 &amp; m <= n &amp; p . m in A )  }  or p . n in A or (p - A) . (n - (card C)) = p . n )
proofend;

Lm13:  for l being Nat
for p being FinSequence
for A being set st len p = l holds
for n being Nat 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 &amp; k <= n &amp; p . k in A )  }  or p . n in A or (p - A) . (n - (card B)) = p . n )
proofend;

theorem :: FINSEQ_3:85
for p being FinSequence
for A being set
for n being Nat 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 &amp; k <= n &amp; p . k in A )  }  or p . n in A or (p - A) . (n - (card B)) = p . n )
proofend;

theorem :: FINSEQ_3:86
for p being FinSequence
for D, A being set st p is FinSequence of D holds
p - A is FinSequence of D
proofend;

theorem :: FINSEQ_3:87
for p being FinSequence
for A being set st p is one-to-one holds
p - A is one-to-one
proofend;

theorem Th88: :: FINSEQ_3:88
for p being FinSequence
for A being set st p is one-to-one holds
len (p - A) = (len p) - (card (A /\ (rng p)))
proofend;

theorem Th89: :: FINSEQ_3:89
for p being FinSequence
for A being finite set st p is one-to-one &amp; A c= rng p holds
len (p - A) = (len p) - (card A)
proofend;

theorem :: FINSEQ_3:90
for p being FinSequence
for x being set st p is one-to-one &amp; x in rng p holds
len (p - {x}) = (len p) - 1
proofend;

theorem Th91: :: FINSEQ_3:91
for p, q being FinSequence holds
( ( rng p misses rng q &amp; p is one-to-one &amp; q is one-to-one ) iff p ^ q is one-to-one )
proofend;

theorem :: FINSEQ_3:92
for A being set
for k being Nat st A c= Seg k holds
Sgm A is one-to-one by Lm1;

theorem Th93: :: FINSEQ_3:93
for x being set holds <*x*> is one-to-one
proofend;

theorem Th94: :: FINSEQ_3:94
for x, y being set holds
( x <> y iff <*x,y*> is one-to-one )
proofend;

theorem Th95: :: FINSEQ_3:95
for x, y, z being set holds
( ( x <> y &amp; y <> z &amp; z <> x ) iff <*x,y,z*> is one-to-one )
proofend;

theorem Th96: :: FINSEQ_3:96
for p being FinSequence
for x being set st p is one-to-one &amp; rng p = {x} holds
len p = 1
proofend;

theorem :: FINSEQ_3:97
for p being FinSequence
for x being set st p is one-to-one &amp; rng p = {x} holds
p = <*x*>
proofend;

theorem Th98: :: FINSEQ_3:98
for p being FinSequence
for x, y being set st p is one-to-one &amp; rng p = {x,y} &amp; x <> y holds
len p = 2
proofend;

theorem :: FINSEQ_3:99
for p being FinSequence
for x, y being set st p is one-to-one &amp; rng p = {x,y} &amp; x <> y &amp; not p = <*x,y*> holds
p = <*y,x*>
proofend;

theorem Th100: :: FINSEQ_3:100
for p being FinSequence
for x, y, z being set st p is one-to-one &amp; rng p = {x,y,z} &amp; <*x,y,z*> is one-to-one holds
len p = 3
proofend;

theorem :: FINSEQ_3:101
for p being FinSequence
for x, y, z being set st p is one-to-one &amp; rng p = {x,y,z} &amp; x <> y &amp; y <> z &amp; x <> z holds
len p = 3
proofend;

begin

:: from FSM_1
theorem :: FINSEQ_3:102
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 &amp; df = <*d*> ^ df1 )
proofend;

theorem :: FINSEQ_3:103
for i being Nat
for df being FinSequence
for d being set st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i
proofend;

:: from MATRIX_2, 2005.11.16, A.T.
definition
let i be Nat;
let p be FinSequence;
func Del (p,i) ->  FinSequence equals :: FINSEQ_3:def 2
p * (Sgm ((dom p) \ {i}));
coherence
 p * (Sgm ((dom p) \ {i})) is FinSequence
proofend;
end;

:: deftheorem  defines Del FINSEQ_3:def_2_:_
 for i being Nat
for p being FinSequence holds Del (p,i) = p * (Sgm ((dom p) \ {i}));

theorem Th104: :: FINSEQ_3:104
for i being Nat
for p being FinSequence holds
( ( i in dom p implies ex m being Nat st
( len p = m + 1 &amp; len (Del (p,i)) = m ) ) &amp; ( not i in dom p implies Del (p,i) = p ) )
proofend;

theorem :: FINSEQ_3:105
for i being Nat
for D being non empty set
for p being FinSequence of D holds Del (p,i) is FinSequence of D
proofend;

:: from MATRLIN, 2005.11.16, A.T.
theorem :: FINSEQ_3:106
for i being Nat
for p being FinSequence holds rng (Del (p,i)) c= rng p
proofend;

:: from GOBOARD1, 2005.11.16, A.T.
theorem Th107: :: FINSEQ_3:107
for n, m, i being Nat st n = m + 1 &amp; i in Seg n holds
len (Sgm ((Seg n) \ {i})) = m
proofend;

theorem Th108: :: FINSEQ_3:108
for i, k, m, n being Nat st n = m + 1 &amp; k in Seg n &amp; i in Seg m holds
( ( 1 <= i &amp; i < k implies (Sgm ((Seg n) \ {k})) . i = i ) &amp; ( k <= i &amp; i <= m implies (Sgm ((Seg n) \ {k})) . i = i + 1 ) )
proofend;

theorem Th109: :: FINSEQ_3:109
for m, n being Nat
for f being FinSequence st len f = m + 1 &amp; n in dom f holds
len (Del (f,n)) = m
proofend;

theorem :: FINSEQ_3:110
for k, n being Nat
for f being FinSequence st k < n holds
(Del (f,n)) . k = f . k
proofend;

theorem :: FINSEQ_3:111
for m, n, k being Nat
for f being FinSequence st len f = m + 1 &amp; n in dom f &amp; n <= k &amp; k <= m holds
(Del (f,n)) . k = f . (k + 1)
proofend;

:: from JORDAN3, 2005.11.16, A.T.
theorem Th112: :: FINSEQ_3:112
for k, n being Nat
for f being FinSequence st k <= n holds
(f | n) . k = f . k
proofend;

:: missing, 27.11.2005, A.T.
theorem :: FINSEQ_3:113
for p, q being FinSequence st p c= q holds
q | (len p) = p
proofend;

:: from MATRLIN, 2006.01.06, A.T.
theorem Th114: :: FINSEQ_3:114
for A being set
for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)
proofend;

theorem :: FINSEQ_3:115
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
proofend;

:: Moved from GRAPH_2 by AK on 27.12.2006
theorem :: FINSEQ_3:116
for f being FinSubsequence st f is FinSequence holds
Seq f = f
proofend;

:: Moved from SCMBSORT by AK on 10.10.2007
theorem :: FINSEQ_3:117
for t being FinSequence of INT holds t is FinSequence of REAL
proofend;

:: missing, 2008.02.16, A.T,
theorem :: FINSEQ_3:118
for p, q being FinSequence holds
( len p < len q iff dom p c< dom q )
proofend;

:: from CATALG_1, 2009.09.08, A.T.
theorem Th119: :: FINSEQ_3:119
for A being set
for i being Nat holds
( ( i <> 0 &amp; A = {} ) iff i -tuples_on A = {} )
proofend;

:: from AMISTD_2, 2009.09.08, A.T.
registration
let i be Nat;
let D be set ;
clusteri -tuples_on D ->  with_common_domain ;
coherence
 i -tuples_on D is with_common_domain
proofend;
end;

registration
let i be Nat;
let D be set ;
clusteri -tuples_on D ->  product-like ;
coherence
 i -tuples_on D is product-like
proofend;
end;

begin

theorem :: FINSEQ_3:120
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 &amp; len (f * p) = len p &amp; ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )
proofend;

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 &amp; ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) );
existence
 ex b1 being Relation of (D *) st
for x, y being FinSequence of D holds
( [x,y] in b1 iff ( len x = len y &amp; ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of (D *) st ( for x, y being FinSequence of D holds
( [x,y] in b1 iff ( len x = len y &amp; ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) &amp; ( for x, y being FinSequence of D holds
( [x,y] in b2 iff ( len x = len y &amp; ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ExtendRel FINSEQ_3:def_3_:_
 for D being non empty set
for R being Relation of D
for b3 being Relation of (D *) holds
( b3 = ExtendRel R iff for x, y being FinSequence of D holds
( [x,y] in b3 iff ( len x = len y &amp; ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) );

theorem :: FINSEQ_3:121
for D being non empty set holds ExtendRel (id D) = id (D *)
proofend;

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;
predx is_representatives_FS y means :: FINSEQ_3:def 4
( len x = len y &amp; ( 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_:_
 for D being non empty set
for R being Equivalence_Relation of D
for y being FinSequence of Class R
for x being FinSequence of D holds
( x is_representatives_FS y iff ( len x = len y &amp; ( for n being Element of NAT st n in dom x holds
Class (R,(x . n)) = y . n ) ) );

theorem :: FINSEQ_3:122
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
proofend;

theorem Th123: :: FINSEQ_3:123
for x, X being set holds
( x in product <*X*> iff ex y being set st
( y in X &amp; x = <*y*> ) )
proofend;

theorem Th124: :: FINSEQ_3:124
for z, X, Y being set holds
( z in product <*X,Y*> iff ex x, y being set st
( x in X &amp; y in Y &amp; z = <*x,y*> ) )
proofend;

theorem Th125: :: FINSEQ_3:125
for a, X, Y, Z being set holds
( a in product <*X,Y,Z*> iff ex x, y, z being set st
( x in X &amp; y in Y &amp; z in Z &amp; a = <*x,y,z*> ) )
proofend;

theorem :: FINSEQ_3:126
for D being non empty set holds product <*D*> = 1 -tuples_on D
proofend;

theorem Th127: :: FINSEQ_3:127
for D1, D2 being non empty set holds product <*D1,D2*> =  {  <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum  }
proofend;

theorem :: FINSEQ_3:128
for D being non empty set holds product <*D,D*> = 2 -tuples_on D
proofend;

theorem Th129: :: FINSEQ_3:129
for D1, D2, D3 being non empty set holds product <*D1,D2,D3*> =  {  <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum  }
proofend;

theorem :: FINSEQ_3:130
for D being non empty set holds product <*D,D,D*> = 3 -tuples_on D
proofend;

theorem Th131: :: FINSEQ_3:131
for i being Nat
for D being set holds product (i |-> D) = i -tuples_on D
proofend;

theorem Th132: :: FINSEQ_3:132
for f being Function holds
( doms <*f*> = <*(dom f)*> &amp; rngs <*f*> = <*(rng f)*> )
proofend;

theorem Th133: :: FINSEQ_3:133
for f, g being Function holds
( doms <*f,g*> = <*(dom f),(dom g)*> &amp; rngs <*f,g*> = <*(rng f),(rng g)*> )
proofend;

theorem :: FINSEQ_3:134
for f, g, h being Function holds
( doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> &amp; rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )
proofend;

theorem Th135: :: FINSEQ_3:135
for X being set holds
( Union <*X*> = X &amp; meet <*X*> = X )
proofend;

theorem Th136: :: FINSEQ_3:136
for X, Y being set holds
( Union <*X,Y*> = X \/ Y &amp; meet <*X,Y*> = X /\ Y )
proofend;

theorem :: FINSEQ_3:137
for X, Y, Z being set holds
( Union <*X,Y,Z*> = (X \/ Y) \/ Z &amp; meet <*X,Y,Z*> = (X /\ Y) /\ Z )
proofend;

theorem :: FINSEQ_3:138
for x being set
for f, g, h being Function st x in dom f holds
( <*f*> .. (1,x) = f . x &amp; <*f,g*> .. (1,x) = f . x &amp; <*f,g,h*> .. (1,x) = f . x )
proofend;

theorem :: FINSEQ_3:139
for x being set
for g, f, h being Function st x in dom g holds
( <*f,g*> .. (2,x) = g . x &amp; <*f,g,h*> .. (2,x) = g . x )
proofend;

theorem :: FINSEQ_3:140
for x being set
for h, f, g being Function st x in dom h holds
<*f,g,h*> .. (3,x) = h . x
proofend;

theorem :: FINSEQ_3:141
for h being Function holds
( dom <:<*h*>:> = dom h &amp; ( for x being set st x in dom h holds
<:<*h*>:> . x = <*(h . x)*> ) )
proofend;

theorem Th142: :: FINSEQ_3:142
for f1, f2 being Function holds
( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) &amp; ( for x being set st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )
proofend;

theorem :: FINSEQ_3:143
for h being Function holds
( dom (Frege <*h*>) = product <*(dom h)*> &amp; rng (Frege <*h*>) = product <*(rng h)*> &amp; ( for x being set st x in dom h holds
(Frege <*h*>) . <*x*> = <*(h . x)*> ) )
proofend;

theorem Th144: :: FINSEQ_3:144
for f1, f2 being Function holds
( dom (Frege <*f1,f2*>) = product <*(dom f1),(dom f2)*> &amp; rng (Frege <*f1,f2*>) = product <*(rng f1),(rng f2)*> &amp; ( for x, y being set st x in dom f1 &amp; y in dom f2 holds
(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> ) )
proofend;

theorem :: FINSEQ_3:145
for x being set
for f1, f2 being Function st x in dom f1 &amp; x in dom f2 holds
for y1, y2 being set holds
( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )
proofend;

theorem :: FINSEQ_3:146
for x, y being set
for f1, f2 being Function st x in dom f1 &amp; y in dom f2 holds
for y1, y2 being set holds
( [:f1,f2:] . (x,y) = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> )
proofend;

theorem :: FINSEQ_3:147
for X, Y being set holds Funcs (<*X*>,Y) = <*(Funcs (X,Y))*>
proofend;

theorem :: FINSEQ_3:148
for X, Y, Z being set holds Funcs (<*X,Y*>,Z) = <*(Funcs (X,Z)),(Funcs (Y,Z))*>
proofend;

theorem :: FINSEQ_3:149
for X, Y being set holds Funcs (X,<*Y*>) = <*(Funcs (X,Y))*>
proofend;

theorem :: FINSEQ_3:150
for X, Y, Z being set holds Funcs (X,<*Y,Z*>) = <*(Funcs (X,Y)),(Funcs (X,Z))*>
proofend;

::from JORDAN2C, 2011.07.03, A.T.
theorem :: FINSEQ_3:151
for x, y being set
for f being FinSequence st rng f = {x,y} &amp; len f = 2 &amp; not ( f . 1 = x &amp; f . 2 = y ) holds
( f . 1 = y &amp; f . 2 = x )
proofend;

:: from GLIB_001, 2011.07.30, A.T.
theorem :: FINSEQ_3:152
for X being set
for k being Element of NAT st X c= Seg k holds
for m, n being Element of NAT st m in dom (Sgm X) &amp; n = (Sgm X) . m holds
m <= n
proofend;

registration
let i be Nat;
let D be finite set ;
clusteri -tuples_on D ->  finite ;
coherence
 i -tuples_on D is finite
proofend;
end;