let p, q be FinSequence; :: thesis: for k being Nat st len p = k + 1 & q = p | (Seg k) holds
p = q ^ <*(p . (k + 1))*>
let k be Nat; :: 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: for l being Nat st l in dom q holds
p . l = q . l by A2, FUNCT_1:47;
set r = <*(p . (k + 1))*>;
A4: now :: thesis: for l being Nat st l in dom <*(p . (k + 1))*> holds
p . ((len q) + l) = <*(p . (k + 1))*> . l
let l be 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:2, FINSEQ_1:38;
then A5: l = 1 by TARSKI:def 1;
hence p . ((len q) + l) = p . (k + 1) by A1, A2, Th51
.= <*(p . (k + 1))*> . l by A5, FINSEQ_1:40 ;
:: thesis: verum
end;
len p = (len q) + 1 by A1, A2, Th51
.= (len q) + (len <*(p . (k + 1))*>) by FINSEQ_1:39 ;
hence p = q ^ <*(p . (k + 1))*> by A3, A4, Th36; :: thesis: verum