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 A1: ( 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;
A2: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
( f1 is_continuous_in y & f2 is_continuous_in y ) by A1, NFCONT_4:21;
then A3: ( y in dom f1 & y in dom f2 ) by NFCONT_1:def 6;
then A4: y in dom (f1 (#) f2) by A2, 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
A5: rng s1 c= dom (f1 (#) f2) and
A6: ( 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 A2, XBOOLE_1:17;
then A7: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A5;
then A8: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A6, Lm3;
then (f1 /* s1) (#) (f2 /* s1) is convergent ;
hence (f1 (#) f2) /* s1 is convergent by A2, A5, RFUNCT_2:8; :: thesis: (f1 (#) f2) /. y = lim ((f1 (#) f2) /* s1)
( f1 . y = f1 /. y & f2 . y = f2 /. y ) by A3, PARTFUN1:def 6;
then A9: ( f1 . y = lim (f1 /* s1) & f2 . y = lim (f2 /* s1) ) by A1, A6, A7, Lm3;
thus (f1 (#) f2) /. y = (f1 (#) f2) . y by A4, PARTFUN1:def 6
.= (f1 . y) * (f2 . y) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A9, A8, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A2, A5, RFUNCT_2:8 ; :: thesis: verum
end;
hence g1 (#) g2 is_continuous_in x by Lm3, A4; :: thesis: verum