let D be non empty set ; for i being Nat
for f being FinSequence of D * holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )
let i be Nat; for f being FinSequence of D * holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )
let f be FinSequence of D * ; ( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )
set DC = D -concatenation ;
defpred S1[ Nat] means for i being Nat
for f being FinSequence of D * st len f = $1 holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) );
A1:
S1[ 0 ]
A2:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A3:
S1[
j]
;
S1[j + 1]
set j1 =
j + 1;
let i be
Nat;
for f being FinSequence of D * st len f = j + 1 holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )let f1 be
FinSequence of
D * ;
( len f1 = j + 1 implies ( i in dom ((D -concatenation) "**" f1) iff ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) ) ) )
assume A4:
len f1 = j + 1
;
( i in dom ((D -concatenation) "**" f1) iff ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) ) )
consider f being
FinSequence of
D * ,
d being
Element of
D * such that A5:
f1 = f ^ <*d*>
by FINSEQ_2:19, A4;
A6:
(len f) + 1
= len f1
by A5, FINSEQ_2:16;
A7:
(D -concatenation) "**" f1 =
((D -concatenation) "**" f) ^ ((D -concatenation) "**" <*d*>)
by Th3, A5
.=
((D -concatenation) "**" f) ^ d
by FINSOP_1:11
;
A8:
dom f c= dom f1
by A5, FINSEQ_1:26;
thus
(
i in dom ((D -concatenation) "**" f1) implies ex
n,
k being
Nat st
(
n + 1
in dom f1 &
k in dom (f1 . (n + 1)) &
i = k + (len ((D -concatenation) "**" (f1 | n))) ) )
( ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) ) implies i in dom ((D -concatenation) "**" f1) )
given n,
k being
Nat such that A12:
(
n + 1
in dom f1 &
k in dom (f1 . (n + 1)) &
i = k + (len ((D -concatenation) "**" (f1 | n))) )
;
i in dom ((D -concatenation) "**" f1)
per cases
( n + 1 in dom f or ex j being Nat st
( j in dom <*d*> & n + 1 = (len f) + j ) )
by A12, A5, FINSEQ_1:25;
suppose A13:
n + 1
in dom f
;
i in dom ((D -concatenation) "**" f1)then
( 1
<= n + 1 &
n + 1
<= len f )
by FINSEQ_3:25;
then A14:
n < len f
by NAT_1:13;
A15:
k in dom (f . (n + 1))
by A13, A5, FINSEQ_1:def 7, A12;
i = k + (len ((D -concatenation) "**" (f | n)))
by A12, A14, A5, FINSEQ_5:22;
then A16:
i in dom ((D -concatenation) "**" f)
by A15, A13, A6, A4, A3;
dom ((D -concatenation) "**" f) c= dom ((D -concatenation) "**" f1)
by A7, FINSEQ_1:26;
hence
i in dom ((D -concatenation) "**" f1)
by A16;
verum end; end;
end;
for j being Nat holds S1[j]
from NAT_1:sch 2(A1, A2);
then
S1[ len f]
;
hence
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )
; verum