let m be non empty Element of NAT ; :: thesis: for Z being set
for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g holds
f (#) g is_continuous_on Z
let Z be set ; :: thesis: for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g holds
f (#) g is_continuous_on Z
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g implies f (#) g is_continuous_on Z )
assume A1: ( f is_continuous_on Z & g is_continuous_on Z ) ; :: thesis: ( not Z c= dom f or not Z c= dom g or f (#) g is_continuous_on Z )
assume AK: ( Z c= dom f & Z c= dom g ) ; :: thesis: f (#) g is_continuous_on Z
reconsider f1 = f, g1 = g as PartFunc of (REAL-NS m),REAL by REAL_NS1:def 4;
P2: Z c= (dom f1) /\ (dom g1) by AK, XBOOLE_1:19;
AA: dom (f1 (#) g1) = (dom f1) /\ (dom g1) by VALUED_1:def 4;

now :: thesis: for s1 being sequence of (REAL-NS m) st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( (f1 (#) g1) /* s1 is convergent & (f1 (#) g1) /. (lim s1) = lim ((f1 (#) g1) /* s1) )

let s1 be sequence of (REAL-NS m); :: thesis: ( rng s1 c= Z & s1 is convergent & lim s1 in Z implies ( (f1 (#) g1) /* s1 is convergent & (f1 (#) g1) /. (lim s1) = lim ((f1 (#) g1) /* s1) ) )
assume A23: ( rng s1 c= Z & s1 is convergent & lim s1 in Z ) ; :: thesis: ( (f1 (#) g1) /* s1 is convergent & (f1 (#) g1) /. (lim s1) = lim ((f1 (#) g1) /* s1) )
then A25: ( f1 /* s1 is convergent & g1 /* s1 is convergent ) by AK, XTh360C, A1;
then A28: (f1 /* s1) (#) (g1 /* s1) is convergent ;
A26: rng s1 c= (dom f1) /\ (dom g1) by P2, A23, XBOOLE_1:1;
hence (f1 (#) g1) /* s1 is convergent by A28, RFUNCT_2:8; :: thesis: (f1 (#) g1) /. (lim s1) = lim ((f1 (#) g1) /* s1)
set y = lim s1;
( f1 . (lim s1) = f1 /. (lim s1) & g1 . (lim s1) = g1 /. (lim s1) ) by A23, AK, PARTFUN1:def 6;
then A29: ( f1 . (lim s1) = lim (f1 /* s1) & g1 . (lim s1) = lim (g1 /* s1) ) by A23, AK, XTh360C, A1;
thus (f1 (#) g1) /. (lim s1) = (f1 (#) g1) . (lim s1) by A23, P2, AA, PARTFUN1:def 6
.= (f1 . (lim s1)) * (g1 . (lim s1)) by VALUED_1:5
.= lim ((f1 /* s1) (#) (g1 /* s1)) by A29, A25, SEQ_2:15
.= lim ((f1 (#) g1) /* s1) by A26, RFUNCT_2:8 ; :: thesis: verum

end;

hence f (#) g is_continuous_on Z by P2, AA, XTh360C; :: thesis: verum