theorem Th46: :: NUMBER19:46

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
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))))*>