let p be FinSequence; :: thesis: for i being Nat st i + 1 <= len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
let i be Nat; :: thesis: ( i + 1 <= len p implies p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> )
assume A1: i + 1 <= len p ; :: thesis: p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
then A2: len (p | (i + 1)) = i + 1 by FINSEQ_1:59;
i < len p by A1, NAT_1:13;
then A3: ( len (p | i) = i & len <*(p . (i + 1))*> = 1 ) by FINSEQ_1:40, FINSEQ_1:59;
then A4: len ((p | i) ^ <*(p . (i + 1))*>) = i + 1 by FINSEQ_1:22;
thus len (p | (i + 1)) = len ((p | i) ^ <*(p . (i + 1))*>) by A1, A4, FINSEQ_1:59; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (p | (i + 1)) or (p | (i + 1)) . b₁ = ((p | i) ^ <*(p . (i + 1))*>) . b₁ )
let j be Nat; :: thesis: ( not 1 <= j or not j <= len (p | (i + 1)) or (p | (i + 1)) . j = ((p | i) ^ <*(p . (i + 1))*>) . j )
assume A5: ( 1 <= j & j <= len (p | (i + 1)) ) ; :: thesis: (p | (i + 1)) . j = ((p | i) ^ <*(p . (i + 1))*>) . j

per cases ( j <= i or j = i + 1 ) by A5, A2, NAT_1:8;

suppose A6: j <= i ; :: thesis: (p | (i + 1)) . j = ((p | i) ^ <*(p . (i + 1))*>) . j

A7: j in dom (p | i) by A3, A5, A6, FINSEQ_3:25;
thus (p | (i + 1)) . j = p . j by A2, A5, FINSEQ_1:1, FUNCT_1:49
.= (p | i) . j by A6, A5, FINSEQ_1:1, FUNCT_1:49
.= ((p | i) ^ <*(p . (i + 1))*>) . j by A7, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A8: j = i + 1 ; :: thesis: (p | (i + 1)) . j = ((p | i) ^ <*(p . (i + 1))*>) . j

then j >= 1 by NAT_1:11;
hence (p | (i + 1)) . j = p . (i + 1) by A8, FINSEQ_1:1, FUNCT_1:49
.= ((p | i) ^ <*(p . (i + 1))*>) . j by A3, A8, FINSEQ_1:42 ;
:: thesis: verum

end;

end;