theorem :: FINSEQOP:11

for D, D9, E being non empty set
for i, j being natural Number
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))