let S, T, V be RealNormSpace; :: thesis: for x0 being Point of V
for f1 being PartFunc of the carrier of V, the carrier of S
for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let x0 be Point of V; :: thesis: for f1 being PartFunc of the carrier of V, the carrier of S
for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of the carrier of V, the carrier of S; :: thesis: for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of the carrier of S, the carrier of T; :: thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; :: thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; :: thesis: f2 * f1 is_continuous_in x0
thus x0 in dom (f2 * f1) by A1; :: according to NFCONT_1:def 5 :: thesis: for b1 being Element of bool [:NAT, the carrier of V:] holds
( not rng b1 c= dom (f2 * f1) or not b1 is convergent or not lim b1 = x0 or ( (f2 * f1) /* b1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* b1) ) )
let s1 be sequence of V; :: thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
B6: rng (f1 /* s1) c= dom f2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f1 /* s1) or x in dom f2 )
assume x in rng (f1 /* s1) ; :: thesis: x in dom f2
then consider n being Element of NAT such that
A7: x = (f1 /* s1) . n by FUNCT_2:113;
s1 . n in rng s1 by VALUED_0:28;
then f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence x in dom f2 by A4, A6, A7, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum
end;
A9: now :: thesis: for n being Element of NAT holds ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
let n be Element of NAT ; :: thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by B6, FUNCT_2:108 ; :: thesis: verum
end;
then A10: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A11: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_1:def 5;
(f2 * f1) /. x0 = f2 /. (f1 /. x0) by A1, PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A3, B6, A11, NFCONT_1:def 5
.= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ;
hence ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) by A3, B6, A10, A11, NFCONT_1:def 5; :: thesis: verum