theorem :: FINSEQOP:84

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 holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))