theorem Th140: :: FINSEQ_3:142

for f1, f2 being Function holds
( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being object st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )