let n, m be non zero Element of NAT ; :: thesis: for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
set S = REAL-NS n;
set T = REAL-NS m;
let R1 be RestFunc of (REAL-NS n); :: thesis: ( R1 /. 0 = 0. (REAL-NS n) implies for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) )
assume R1 /. 0 = 0. (REAL-NS n) ; :: thesis: for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
then consider d0 being Real such that
A1: 0 < d0 and
A2: for h being Real st |.h.| < d0 holds
||.(R1 /. h).|| <= 1 * |.h.| by Th46;
let R2 be RestFunc of (REAL-NS n),(REAL-NS m); :: thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) )
assume A3: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; :: thesis: for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
let L be LinearFunc of (REAL-NS n); :: thesis: R2 * (L + R1) is RestFunc of (REAL-NS m)
consider r being Point of (REAL-NS n) such that
A4: for h being Real holds L /. h = h * r by NDIFF_3:def 2;
set K = ||.r.||;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def 2;
then A5: rng (L + R1) c= dom R2 ;
R1 is total by NDIFF_3:def 1;
then A6: L + R1 is total by VFUNCT_1:32;
then A7: dom (L + R1) = REAL by PARTFUN1:def 2;
dom (R2 * (L + R1)) = dom (L + R1) by A5, RELAT_1:27
.= REAL by A6, PARTFUN1:def 2 ;
then R2 * (L + R1) is total by PARTFUN1:def 2;
hence R2 * (L + R1) is RestFunc of (REAL-NS m) by A8, Th23; :: thesis: verum