theorem Th43: :: NUMBER19:43

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z1, z2 being FinSequence of the carrier of L
for f1, f2 being NAT -valued FinSequence st len f1 = len z1 & len f2 <= len z2 holds
rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2))