let i be Element of 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) ) )
set q' = q ^ <*c*>;
assume A1: ( p = (q ^ <*c*>) ^ r & i = (len q) + 1 ) ; :: thesis: ( ( for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
then A2: p = q ^ (<*c*> ^ r) by FINSEQ_1:45;
A3: len (q ^ <*c*>) = i by A1, FINSEQ_2:19;
A4: len p = (len (q ^ <*c*>)) + (len r) by A1, FINSEQ_1:35;
thus for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l :: thesis: ( p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )

proof

let l be Element of 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:27;
hence p . l = q . l by A2, FINSEQ_1:def 7; :: thesis: verum

end;

i in Seg i by A1, FINSEQ_1:5;
then i in dom (q ^ <*c*>) by A3, FINSEQ_1:def 3;
hence p . i = (q ^ <*c*>) . i by A1, FINSEQ_1:def 7
.= c by A1, FINSEQ_1:59 ;
:: thesis: for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i)
thus for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) by A1, A3, A4, FINSEQ_1:36; :: thesis: verum