let m be non zero 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 A2: ( 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;
A3: Z c= (dom f1) /\ (dom g1) by A2, XBOOLE_1:19;
A4: 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 A5: ( 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 A6: ( f1 /* s1 is convergent & g1 /* s1 is convergent ) by A2, Th43, A1;
then A7: (f1 /* s1) (#) (g1 /* s1) is convergent ;
A8: rng s1 c= (dom f1) /\ (dom g1) by A3, A5;
hence (f1 (#) g1) /* s1 is convergent by A7, 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 A5, A2, PARTFUN1:def 6;
then A9: ( f1 . (lim s1) = lim (f1 /* s1) & g1 . (lim s1) = lim (g1 /* s1) ) by A5, A2, Th43, A1;
thus (f1 (#) g1) /. (lim s1) = (f1 (#) g1) . (lim s1) by A5, A3, A4, PARTFUN1:def 6
.= (f1 . (lim s1)) * (g1 . (lim s1)) by VALUED_1:5
.= lim ((f1 /* s1) (#) (g1 /* s1)) by A9, A6, SEQ_2:15
.= lim ((f1 (#) g1) /* s1) by A8, RFUNCT_2:8 ; :: thesis: verum
end;
hence f (#) g is_continuous_on Z by A3, A4, Th43; :: thesis: verum