let i be Nat; :: thesis: for D being non empty set
for c being Element of D
for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let D be non empty set ; :: thesis: for c being Element of D
for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let c be Element of D; :: thesis: for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let p, q, r be FinSequence of D; :: thesis: ( p = (q ^ <*c*>) ^ r & i = (len q) + 1 implies ( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) ) )
set q9 = q ^ <*c*>;
assume that
A1: p = (q ^ <*c*>) ^ r and
A2: i = (len q) + 1 ; :: thesis: ( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
A3: p = q ^ (<*c*> ^ r) by A1, FINSEQ_1:32;
thus for l being Nat st 1 <= l & l <= len q holds
p . l = q . l :: thesis: ( p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )

proof

let l be Nat; :: thesis: ( 1 <= l & l <= len q implies p . l = q . l )
assume ( 1 <= l & l <= len q ) ; :: thesis: p . l = q . l
then l in dom q by FINSEQ_3:25;
hence p . l = q . l by A3, FINSEQ_1:def 7; :: thesis: verum

end;

A4: len (q ^ <*c*>) = i by A2, FINSEQ_2:16;
i in Seg i by A2, FINSEQ_1:3;
then i in dom (q ^ <*c*>) by A4, FINSEQ_1:def 3;
hence p . i = (q ^ <*c*>) . i by A1, FINSEQ_1:def 7
.= c by A2, FINSEQ_1:42 ;
:: thesis: for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i)
len p = (len (q ^ <*c*>)) + (len r) by A1, FINSEQ_1:22;
hence for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) by A1, A4, FINSEQ_1:23; :: thesis: verum