let p, q be FinSequence; :: thesis: for k being natural number st len p = k + 1 & q = p | (Seg k) holds
p = q ^ <*(p . (k + 1))*>
let k be natural number ; :: thesis: ( len p = k + 1 & q = p | (Seg k) implies p = q ^ <*(p . (k + 1))*> )
assume that
A1: len p = k + 1 and
A2: q = p | (Seg k) ; :: thesis: p = q ^ <*(p . (k + 1))*>
A3: len p = (len q) + 1 by A1, A2, Th59
.= (len q) + (len <*(p . (k + 1))*>) by FINSEQ_1:56 ;
set r = <*(p . (k + 1))*>;
A4: for l being Element of NAT st l in dom q holds
p . l = q . l by A2, FUNCT_1:70;

now

let l be Element of NAT ; :: thesis: ( l in dom <*(p . (k + 1))*> implies p . ((len q) + l) = <*(p . (k + 1))*> . l )
assume l in dom <*(p . (k + 1))*> ; :: thesis: p . ((len q) + l) = <*(p . (k + 1))*> . l
then l in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A5: l = 1 by TARSKI:def 1;
hence p . ((len q) + l) = p . (k + 1) by A1, A2, Th59
.= <*(p . (k + 1))*> . l by A5, FINSEQ_1:57 ;
:: thesis: verum

end;

hence p = q ^ <*(p . (k + 1))*> by A3, A4, Th43; :: thesis: verum