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) ) )

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

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

A4:
len (q ^ <*c*>) = i
by A2, FINSEQ_2:16;
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;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

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