let i be Element of NAT ; :: thesis: for f, g being PartFunc of (REAL i),REAL
for x being Element of REAL i st f is_continuous_in x & g is_continuous_in x holds
f (#) g is_continuous_in x
let g1, g2 be PartFunc of (REAL i),REAL; :: thesis: for x being Element of REAL i st g1 is_continuous_in x & g2 is_continuous_in x holds
g1 (#) g2 is_continuous_in x
let x be Element of REAL i; :: thesis: ( g1 is_continuous_in x & g2 is_continuous_in x implies g1 (#) g2 is_continuous_in x )
assume A2: ( g1 is_continuous_in x & g2 is_continuous_in x ) ; :: thesis: g1 (#) g2 is_continuous_in x
reconsider y = x as Point of (REAL-NS i) by REAL_NS1:def 4;
reconsider f1 = g1, f2 = g2 as PartFunc of (REAL-NS i),REAL by REAL_NS1:def 4;
A3: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
( f1 is_continuous_in y & f2 is_continuous_in y ) by A2, NFCONT_4:21;
then X1: ( y in dom f1 & y in dom f2 ) by NFCONT_1:def 6;
then X2: y in dom (f1 (#) f2) by A3, XBOOLE_0:def 4;

now :: thesis: for s1 being sequence of (REAL-NS i) st rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = y holds
( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. y = lim ((f1 (#) f2) /* s1) )

let s1 be sequence of (REAL-NS i); :: thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = y implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. y = lim ((f1 (#) f2) /* s1) ) )
assume that
A22: rng s1 c= dom (f1 (#) f2) and
A23: ( s1 is convergent & lim s1 = y ) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. y = lim ((f1 (#) f2) /* s1) )
( dom (f1 (#) f2) c= dom f1 & dom (f1 (#) f2) c= dom f2 ) by A3, XBOOLE_1:17;
then A24: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A22, XBOOLE_1:1;
then A25: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A2, A23, XTh360;
then (f1 /* s1) (#) (f2 /* s1) is convergent ;
hence (f1 (#) f2) /* s1 is convergent by A3, A22, RFUNCT_2:8; :: thesis: (f1 (#) f2) /. y = lim ((f1 (#) f2) /* s1)
( f1 . y = f1 /. y & f2 . y = f2 /. y ) by X1, PARTFUN1:def 6;
then A29: ( f1 . y = lim (f1 /* s1) & f2 . y = lim (f2 /* s1) ) by A2, A23, A24, XTh360;
thus (f1 (#) f2) /. y = (f1 (#) f2) . y by X2, PARTFUN1:def 6
.= (f1 . y) * (f2 . y) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A29, A25, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A3, A22, RFUNCT_2:8 ; :: thesis: verum

end;

hence g1 (#) g2 is_continuous_in x by XTh360, X2; :: thesis: verum