theorem Th52: :: NUMBER17:52

for f1, f2, g1, g2, h1, h2 being complex-valued FinSequence st len f1 = len g1 & len g1 = len h1 holds
((f1 ^ f2) (#) (g1 ^ g2)) (#) (h1 ^ h2) = ((f1 (#) g1) (#) h1) ^ ((f2 (#) g2) (#) h2)