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 17 :: thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len (p | (i + 1)) or (p | (i + 1)) . b1 = ((p | i) ^ <*(p . (i + 1))*>) . b1 )
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;