theorem ThTF3C3: :: ZMODUL05:41

for V, W being non empty set
for f, g being b₁ -valued FinSequence
for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)