:: FINSEQ_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FINSEQ_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 3 = {1,2,3}
proof end;

theorem Th2: :: FINSEQ_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 4 = {1,2,3,4}
proof end;

theorem Th3: :: FINSEQ_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 5 = {1,2,3,4,5}
proof end;

theorem Th4: :: FINSEQ_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 6 = {1,2,3,4,5,6}
proof end;

theorem Th5: :: FINSEQ_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 7 = {1,2,3,4,5,6,7}
proof end;

theorem :: FINSEQ_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Seg 8 = {1,2,3,4,5,6,7,8}
proof end;

theorem :: FINSEQ_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds
( Seg k = {} iff not k in Seg k ) by FINSEQ_1:4, FINSEQ_1:5;

theorem :: FINSEQ_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: FINSEQ_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds not k + 1 in Seg k
proof end;

theorem :: FINSEQ_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number st k <> 0 holds
k in Seg (k + n)
proof end;

theorem Th11: :: FINSEQ_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number st k + n in Seg k holds
n = 0
proof end;

theorem :: FINSEQ_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number st k < n holds
k + 1 in Seg n
proof end;

theorem Th13: :: FINSEQ_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number holds
( k - n in Seg k iff n < k )
proof end;

theorem Th15: :: FINSEQ_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds Seg k misses {(k + 1)}
proof end;

theorem :: FINSEQ_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds (Seg (k + 1)) \ (Seg k) = {(k + 1)}
proof end;

theorem :: FINSEQ_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds Seg k <> Seg (k + 1)
proof end;

theorem :: FINSEQ_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number st Seg k = Seg (k + n) holds
n = 0
proof end;

theorem Th19: :: FINSEQ_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number holds Seg k c= Seg (k + n)
proof end;

theorem Th20: :: FINSEQ_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being natural number holds Seg k, Seg n are_c=-comparable
proof end;

theorem :: FINSEQ_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th22: :: FINSEQ_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for k being natural number st Seg k = {y} holds
( k = 1 & y = 1 )
proof end;

theorem :: FINSEQ_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence
for x being set st x in dom p holds
x in dom (p ^ q)
proof end;

theorem Th25: :: FINSEQ_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for x being set st x in dom p holds
x is Nat
proof end;

theorem Th26: :: FINSEQ_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for x being set st x in dom p holds
x <> 0
proof end;

theorem Th27: :: FINSEQ_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for n being natural number holds
( n in dom p iff ( n - 1 is Nat & (len p) - n is Nat ) )
proof end;

theorem Th29: :: FINSEQ_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds dom <*x,y*> = Seg 2
proof end;

theorem Th30: :: FINSEQ_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds dom <*x,y,z*> = Seg 3
proof end;

theorem :: FINSEQ_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds
( len p = len q iff dom p = dom q )
proof end;

theorem :: FINSEQ_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds
( len p <= len q iff dom p c= dom q )
proof end;

theorem Th33: :: FINSEQ_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for x being set st x in rng p holds
1 in dom p
proof end;

theorem :: FINSEQ_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence st rng p <> {} holds
1 in dom p
proof end;

theorem :: FINSEQ_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSEQ_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSEQ_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th38: :: FINSEQ_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds {} <> <*x,y*>
proof end;

theorem :: FINSEQ_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds {} <> <*x,y,z*>
proof end;

theorem Th40: :: FINSEQ_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds <*x*> <> <*y,z*>
proof end;

theorem :: FINSEQ_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for u, x, y, z being set holds <*u*> <> <*x,y,z*>
proof end;

theorem :: FINSEQ_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for u, v, x, y, z being set holds <*u,v*> <> <*x,y,z*>
proof end;

theorem Th43: :: FINSEQ_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, p, q being FinSequence st len r = (len p) + (len q) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th48: :: FINSEQ_3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Sgm {} = {}
proof end;

theorem :: FINSEQ_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st 0 <> n holds
Sgm {n} = <*n*>
proof end;

theorem :: FINSEQ_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being natural number st 0 < n & n < m holds
Sgm {n,m} = <*n,m*>
proof end;

theorem Th52: :: FINSEQ_3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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: ( ( for k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ) implies for k being natural number holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) )
assume A1: for k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ; :: thesis: for k being natural number holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
let k be natural number ; :: thesis: (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
set X = Sgm (Seg (k + (n + 1)));
set Y = Sgm (Seg (k + 1));
Sgm (Seg (k + (n + 1))) = Sgm (Seg ((k + 1) + n)) ;
then A2: (Sgm (Seg (k + (n + 1)))) | (Seg (k + 1)) = Sgm (Seg (k + 1)) by A1;
(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: rng (Sgm (Seg (k + 1))) = Seg (k + 1) by FINSEQ_1:def 13;
A4: Sgm (Seg (k + 1)) is one-to-one by Lm1;
A5: len (Sgm (Seg (k + 1))) = k + 1 by Th52;
then A6: ( dom (Sgm (Seg (k + 1))) = Seg (k + 1) & k <= k + 1 ) by FINSEQ_1:def 3, NAT_1:37;
then A7: dom p = Seg k by A5, FINSEQ_1:21;
A8: (Sgm (Seg (k + 1))) . (k + 1) = k + 1
proof
assume A9: not (Sgm (Seg (k + 1))) . (k + 1) = k + 1 ; :: thesis: contradiction
k + 1 in dom (Sgm (Seg (k + 1))) by A6, FINSEQ_1:6;
then ( (Sgm (Seg (k + 1))) . (k + 1) in Seg (k + 1) & not (Sgm (Seg (k + 1))) . (k + 1) in {(k + 1)} ) by A3, A9, FUNCT_1:def 5, TARSKI:def 1;
then (Sgm (Seg (k + 1))) . (k + 1) in (Seg (k + 1)) \ {(k + 1)} by XBOOLE_0:def 4;
then A10: (Sgm (Seg (k + 1))) . (k + 1) in Seg k by FINSEQ_1:12;
then reconsider n = (Sgm (Seg (k + 1))) . (k + 1) as Nat ;
k + 1 in rng (Sgm (Seg (k + 1))) by A3, 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 Nat by A11;
A13: ( 1 <= x & x <= k + 1 ) by A5, A11, Th27;
now
assume x = k + 1 ; :: thesis: contradiction
then ( n = k + 1 & n <= k & k < k + 1 ) by A10, A12, FINSEQ_1:3, XREAL_1:31;
hence contradiction ; :: thesis: verum
end;
then x < k + 1 by A13, REAL_1:def 5;
then ( k + 1 < n & n <= k & k < k + 1 ) by A5, A10, A12, A13, FINSEQ_1:3, FINSEQ_1:def 13, XREAL_1:31;
hence contradiction by XREAL_1:2; :: thesis: verum
end;
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: (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} c= rng p
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} )
assume A14: x in rng p ; :: thesis: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
A15: rng p c= rng (Sgm (Seg (k + 1))) by FUNCT_1:76;
now
assume A16: x in {(k + 1)} ; :: thesis: contradiction
consider y being set such that
A17: y in dom p and
A18: p . y = x by A14, FUNCT_1:def 5;
reconsider y = y as Nat by A17;
Seg k c= Seg (k + 1) by Th19;
then A19: ( y in dom (Sgm (Seg (k + 1))) & (Sgm (Seg (k + 1))) . y = p . y & x = k + 1 & k + 1 in dom (Sgm (Seg (k + 1))) ) by A6, A7, A16, A17, FINSEQ_1:6, FUNCT_1:70, TARSKI:def 1;
( y <= k & k < k + 1 ) by A7, A17, FINSEQ_1:3, XREAL_1:31;
hence contradiction by A4, A8, A18, A19, FUNCT_1:def 8; :: thesis: verum
end;
hence x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} by A8, A14, A15, XBOOLE_0:def 4; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} or x in rng p )
assume A20: 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 4;
then consider y being set such that
A21: y in dom (Sgm (Seg (k + 1))) and
A22: (Sgm (Seg (k + 1))) . y = x by FUNCT_1:def 5;
now
assume y in {(k + 1)} ; :: thesis: contradiction
then ( x = k + 1 & not x in {(k + 1)} ) by A8, A20, A22, TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
then y in (Seg (k + 1)) \ {(k + 1)} by A6, A21, XBOOLE_0:def 4;
then A23: y in dom p by A7, FINSEQ_1:12;
then p . y = (Sgm (Seg (k + 1))) . y by FUNCT_1:70;
hence x in rng p by A22, A23, FUNCT_1:def 5; :: thesis: verum
end;
then A24: rng p = Seg k by A3, A8, FINSEQ_1:12;
now
let i, j, l, m be natural number ;
assume that
A25: ( 1 <= i & i < j & j <= len p ) and
A26: ( l = p . i & m = p . j ) ; :: thesis: l < m
A27: ( len p = k & i <= len p & 1 <= j ) by A5, A6, A25, XREAL_1:2, FINSEQ_1:21;
then ( i in dom p & j in dom p & len (Sgm (Seg (k + 1))) = k + 1 & k <= k + 1 ) by A7, A25, Th52, FINSEQ_1:3, NAT_1:37;
then ( p . i = (Sgm (Seg (k + 1))) . i & p . j = (Sgm (Seg (k + 1))) . j & j <= len (Sgm (Seg (k + 1))) ) by A25, A27, XREAL_1:2, FUNCT_1:70;
hence l < m by A25, A26, FINSEQ_1:def 13; :: thesis: verum
end;
hence (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by A24, FINSEQ_1:def 13; :: thesis: verum
end;
then ( Sgm (Seg k) = (Sgm (Seg (k + (n + 1)))) | ((Seg (k + 1)) /\ (Seg k)) & k <= k + 1 ) by A2, NAT_1:37, RELAT_1:100;
hence (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) by FINSEQ_1:9; :: thesis: verum
end;

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

theorem :: FINSEQ_3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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: ( 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 FINSEQ_2:55;
then A3: len (Sgm (Seg (k + 1))) = len (idseq (k + 1)) by Th52;
now
let j be Nat; :: thesis: ( j in Seg (k + 1) implies (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j )
assume A4: j in Seg (k + 1) ; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
then A5: j in (Seg k) \/ {(k + 1)} by FINSEQ_1:11;
now
per cases ( j in Seg k or j in {(k + 1)} ) by A5, XBOOLE_0:def 2;
suppose A6: j in Seg k ; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
then ( (Sgm (Seg k)) . j = j & (idseq k) . j = j & (idseq (k + 1)) . j = j & (Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) & dom (Sgm (Seg (k + 1))) = Seg (k + 1) ) by A1, A2, A3, A4, Lm4, FINSEQ_1:def 3, FINSEQ_2:56;
hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A6, FUNCT_1:72; :: thesis: verum
end;
suppose j in {(k + 1)} ; :: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
then A7: j = k + 1 by TARSKI:def 1;
then A8: j in Seg (k + 1) by FINSEQ_1:6;
set X = Sgm (Seg (k + 1));
set Y = Sgm (Seg k);
now
assume (Sgm (Seg (k + 1))) . j <> j ; :: thesis: contradiction
then A9: ( not (Sgm (Seg (k + 1))) . j in {j} & Seg (k + 1) c= Seg (k + 1) ) by TARSKI:def 1;
A10: ( rng (Sgm (Seg (k + 1))) = Seg (k + 1) & dom (Sgm (Seg (k + 1))) = Seg (k + 1) ) by A2, A3, FINSEQ_1:def 3, FINSEQ_1:def 13;
then A11: (Sgm (Seg (k + 1))) . j in Seg (k + 1) by A4, FUNCT_1:def 5;
then (Sgm (Seg (k + 1))) . j in (Seg (k + 1)) \ {(k + 1)} by A7, A9, XBOOLE_0:def 4;
then A12: (Sgm (Seg (k + 1))) . j in Seg k by FINSEQ_1:12;
then reconsider n = (Sgm (Seg (k + 1))) . j as Nat ;
A13: Sgm (Seg (k + 1)) is one-to-one by Lm1;
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k) by Lm4;
then A14: (Sgm (Seg (k + 1))) . n = (Sgm (Seg k)) . n by A12, FUNCT_1:72
.= n by A1, A12, FINSEQ_2:56 ;
( n <= k & k < k + 1 ) by A12, FINSEQ_1:3, XREAL_1:31;
hence contradiction by A7, A8, A10, A11, A13, A14, FUNCT_1:def 8; :: thesis: verum
end;
hence (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j by A8, FINSEQ_2:56; :: 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 A2, A3, FINSEQ_2:10; :: thesis: verum
end;

theorem Th54: :: FINSEQ_3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being natural number holds Sgm (Seg k) = idseq k
proof end;

theorem Th55: :: FINSEQ_3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being natural number holds (idseq (n + k)) | (Seg n) = idseq n
proof end;

theorem :: FINSEQ_3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being natural number holds
( (idseq n) | (Seg m) = idseq m iff m <= n )
proof end;

theorem :: FINSEQ_3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being natural number holds
( (idseq n) | (Seg m) = idseq n iff n <= m )
proof end;

theorem Th59: :: FINSEQ_3:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for X being set holds
( p | X is FinSequence iff ex k being Nat st X /\ (dom p) = Seg k )
proof end;

theorem Th63: :: FINSEQ_3:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
p * (Sgm ((dom p) \ (p " A))) is FinSequence
proof end;
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 :: FINSEQ_3:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th66: :: FINSEQ_3:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds len (p - A) = (len p) - (card (p " A))
proof end;

theorem Th67: :: FINSEQ_3:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds len (p - A) <= len p
proof end;

theorem Th68: :: FINSEQ_3:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds dom (p - A) c= dom p
proof end;

theorem :: FINSEQ_3:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds rng (p - A) = (rng p) \ A
proof end;

theorem :: FINSEQ_3:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds rng (p - A) c= rng p
proof end;

theorem :: FINSEQ_3:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds
( p - A = {} iff rng p c= A )
proof end;

theorem Th76: :: FINSEQ_3:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for A being set holds
( p - A = p iff A misses rng p )
proof end;

theorem :: FINSEQ_3:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for x being set holds
( p - {x} = p iff not x in rng p )
proof end;

theorem :: FINSEQ_3:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds p - {} = p
proof end;

theorem :: FINSEQ_3:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds p - (rng p) = {} by Th75;

Lm6: for A being set holds {} - A = {}
proof end;

Lm7: for x, A being set holds
( <*x*> - A = <*x*> iff not x in A )
proof end;

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

Lm9: for p being FinSequence
for A being set holds (p ^ {} ) - A = (p - A) ^ ({} - A)
proof end;

Lm10: for p being FinSequence
for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
proof end;

Lm11: now
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:45
.= ((p ^ q) - A) ^ (<*x*> - A) by Lm10
.= ((p - A) ^ (q - A)) ^ (<*x*> - A) by A1
.= (p - A) ^ ((q - A) ^ (<*x*> - A)) by FINSEQ_1:45
.= (p - A) ^ ((q ^ <*x*>) - A) by Lm10 ; :: thesis: verum
end;

Lm12: for q, p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A)
proof end;

theorem :: FINSEQ_3:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) by Lm12;

theorem :: FINSEQ_3:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds {} - A = {} by Lm6;

theorem :: FINSEQ_3:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, A being set holds
( <*x*> - A = <*x*> iff not x in A ) by Lm7;

theorem :: FINSEQ_3:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, A being set holds
( <*x*> - A = {} iff x in A ) by Lm8;

theorem Th84: :: FINSEQ_3:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, A being set holds
( <*x,y*> - A = {} iff ( x in A & y in A ) )
proof end;

theorem Th85: :: FINSEQ_3:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm13: for p being FinSequence
for A being set st len p = 0 holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is 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;

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

Lm15: 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds idseq n is one-to-one
proof end;

theorem :: FINSEQ_3:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th102: :: FINSEQ_3:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds <*x*> is one-to-one
proof end;

theorem Th103: :: FINSEQ_3:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( x <> y iff <*x,y*> is one-to-one )
proof end;

theorem Th104: :: FINSEQ_3:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: FINSEQ_3:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def2: :: FINSEQ_3:def 2
p * (Sgm ((dom p) \ {i}));
coherence
p * (Sgm ((dom p) \ {i})) is FinSequence
proof end;
end;

:: deftheorem Def2 defines Del FINSEQ_3:def 2 :
for i being natural number
for p being FinSequence holds Del p,i = p * (Sgm ((dom p) \ {i}));

theorem Th8: :: FINSEQ_3:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th9: :: FINSEQ_3:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being natural number
for p being FinSequence holds rng (Del p,i) c= rng p
proof end;

theorem Th4: :: FINSEQ_3:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th5: :: FINSEQ_3:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th6: :: FINSEQ_3:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence
for n, m being natural number st len f = m + 1 & n in dom f holds
len (Del f,n) = m
proof end;

theorem Th117: :: FINSEQ_3:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence
for n, m, k being Nat st len f = m + 1 & k < n holds
(Del f,n) . k = f . k
proof end;

theorem Th9: :: FINSEQ_3:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence
for n, m, k being Nat st len f = m + 1 & n in dom f & n <= k & k <= m holds
(Del f,n) . k = f . (k + 1)
proof end;

theorem :: FINSEQ_3:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number
for D being set
for f being FinSequence of D
for k being Nat st k <= n holds
(f | n) . k = f . k
proof end;