let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for n being Nat st n < len f holds
rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>
let z be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence
for n being Nat st n < len f holds
rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>
let f be NAT -valued FinSequence; :: thesis: for n being Nat st n < len f holds
rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>
let n be Nat; :: thesis: ( n < len f implies rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*> )
assume A1: n < len f ; :: thesis: rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>
n + 1 <= len f by A1, NAT_1:13;
then A2: ( len (rpoly ((f | (n + 1)),z)) = len (f | (n + 1)) & len (f | (n + 1)) = n + 1 ) by FINSEQ_1:59, Def1;
A3: ( len (rpoly ((f | n),z)) = len (f | n) & len (f | n) = n ) by A1, FINSEQ_1:59, Def1;
then A4: len ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) = n + 1 by FINSEQ_2:16;
for i being Nat st 1 <= i & i <= n + 1 holds
(rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n + 1 implies (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i )
assume A5: ( 1 <= i & i <= n + 1 ) ; :: thesis: (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i
i in dom (f | (n + 1)) by A5, A2, FINSEQ_3:25;
then A6: ( (f | (n + 1)) /. i = (f | (n + 1)) . i & (f | (n + 1)) . i = f . i & i in dom f ) by RELAT_1:57, FUNCT_1:47, PARTFUN1:def 6;
then A7: f . i = f /. i by PARTFUN1:def 6;
A8: (rpoly ((f | (n + 1)),z)) . i = rpoly (((f | (n + 1)) /. i),(z /. i)) by A5, A2, Def1;

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

suppose i = n + 1 ; :: thesis: (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i

hence (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i by A6, A7, A5, A2, Def1, A3; :: thesis: verum

end;

suppose A9: i <= n ; :: thesis: (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i

then i in dom (f | n) by A5, A3, FINSEQ_3:25;
then A10: ( (f | n) /. i = (f | n) . i & (f | n) . i = f . i ) by FUNCT_1:47, PARTFUN1:def 6;
((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i = (rpoly ((f | n),z)) . i by A5, A3, A9, FINSEQ_1:64;
hence (rpoly ((f | (n + 1)),z)) . i = ((rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>) . i by A5, A6, A8, A10, A3, A9, Def1; :: thesis: verum

end;

end;

end;

hence rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*> by A2, A4, FINSEQ_1:14; :: thesis: verum