theorem Th61: :: HILB10_7:61

for F, G being FinSequence-yielding FinSequence
for f, g being FinSequence st f in doms F & g in doms G holds
(App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g)