theorem :: FINSEQOP:51

for D being non empty set
for i being natural Number
for T1, T2 being Tuple of i,D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) by Th48;