let D be non empty set ; :: thesis: 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; :: thesis: 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 * ; :: thesis: ( 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 S₁[ 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: S₁[ 0 ]

proof

let i be Nat; :: thesis: for f being FinSequence of D * st len f = 0 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 * ; :: thesis: ( len f = 0 implies ( 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))) ) ) )
assume len f = 0 ; :: thesis: ( 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))) ) )
then 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))) ) ) by Lm1; :: thesis: verum

end;

A2: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A3: S₁[j] ; :: thesis: S₁[j + 1]
set j1 = j + 1;
let i be Nat; :: thesis: 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 * ; :: thesis: ( 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 ; :: thesis: ( 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))) ) ) :: thesis: ( 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) )

proof

assume A9: i in dom ((D -concatenation) "**" f1) ; :: thesis: ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )

per cases ( i in dom ((D -concatenation) "**" f) or ex l being Nat st
( l in dom d & i = (len ((D -concatenation) "**" f)) + l ) ) by A9, A7, FINSEQ_1:25;

suppose i in dom ((D -concatenation) "**" f) ; :: thesis: ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )

then consider n, k being Nat such that
A10: ( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) by A6, A4, A3;
take n ; :: thesis: ex k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )
take k ; :: thesis: ( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )
thus ( n + 1 in dom f1 & k in dom (f1 . (n + 1)) ) by A10, A5, A8, FINSEQ_1:def 7; :: thesis: i = k + (len ((D -concatenation) "**" (f1 | n)))
( 1 <= n + 1 & n + 1 <= len f ) by A10, FINSEQ_3:25;
then n <= len f by NAT_1:13;
hence i = k + (len ((D -concatenation) "**" (f1 | n))) by FINSEQ_5:22, A5, A10; :: thesis: verum

end;

suppose ex l being Nat st
( l in dom d & i = (len ((D -concatenation) "**" f)) + l ) ; :: thesis: ex n, k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )

then consider l being Nat such that
A11: ( l in dom d & i = l + (len ((D -concatenation) "**" f)) ) ;
take n = len f; :: thesis: ex k being Nat st
( n + 1 in dom f1 & k in dom (f1 . (n + 1)) & i = k + (len ((D -concatenation) "**" (f1 | n))) )
take l ; :: thesis: ( n + 1 in dom f1 & l in dom (f1 . (n + 1)) & i = l + (len ((D -concatenation) "**" (f1 | n))) )
1 <= n + 1 by NAT_1:11;
hence ( n + 1 in dom f1 & l in dom (f1 . (n + 1)) & i = l + (len ((D -concatenation) "**" (f1 | n))) ) by FINSEQ_1:42, FINSEQ_5:23, A5, A11, A6, FINSEQ_3:25; :: thesis: verum

end;

end;

end;

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

end;

suppose ex j being Nat st
( j in dom <*d*> & n + 1 = (len f) + j ) ; :: thesis: i in dom ((D -concatenation) "**" f1)

then consider j being Nat such that
A17: ( j in dom <*d*> & n + 1 = (len f) + j ) ;
( dom <*d*> = Seg 1 & Seg 1 = {1} ) by FINSEQ_1:2, FINSEQ_1:38;
then j = 1 by A17, TARSKI:def 1;
then ( f1 . (n + 1) = d & f1 | n = f ) by A17, FINSEQ_5:23, A5, FINSEQ_1:42;
hence i in dom ((D -concatenation) "**" f1) by A12, FINSEQ_1:28, A7; :: thesis: verum

end;

end;

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A2);
then S₁[ 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))) ) ) ; :: thesis: verum