set X = dom (f1 (#) f2);
dom (f1 (#) f2) c= (dom f1) /\ (dom f2) by VALUED_1:def 4;
then A17: ( dom (f1 (#) f2) c= dom f1 & dom (f1 (#) f2) c= dom f2 ) by XBOOLE_1:18;
A18: ( f1 | (dom (f1 (#) f2)) is continuous & f2 | (dom (f1 (#) f2)) is continuous ) ;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 in dom (f1 (#) f2) implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) )
assume that
A19: rng s1 c= dom (f1 (#) f2) and
A20: s1 is convergent and
A21: lim s1 in dom (f1 (#) f2) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )
A22: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A17, A18, A19, A20, A21, Th14;
then A23: (f1 /* s1) (#) (f2 /* s1) is convergent by SEQ_2:14;
A24: rng s1 c= (dom f1) /\ (dom f2) by A19, VALUED_1:def 4;
( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A17, A18, A19, A20, A21, Th14;
then (f1 (#) f2) . (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A21, VALUED_1:def 4
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A22, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A24, RFUNCT_2:8 ;
hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) by A24, A23, RFUNCT_2:8; :: thesis: verum

end;

then (f1 (#) f2) | (dom (f1 (#) f2)) is continuous by Th14;
hence for b₁ being PartFunc of REAL,REAL st b₁ = f1 (#) f2 holds
b₁ is continuous by RELAT_1:69; :: thesis: verum