0.F;
thus f is total;
A1: dom f = REAL by FUNCOP_1:19;
now
let h;
now let n be Nat;
A2: rng h c= dom f by A1;
A3: n in NAT by ORDINAL1:def 13;
hence ((h")(#)(f/*h)).n = (h").n*((f/*h).n) by NDIFF_1:def 2
.= (h").n*(f.(h.n)) by A3,A2,FUNCT_2:185
.= 0.F by RLVECT_1:23,FUNCOP_1:13;
end;
then (h")(#)(f/*h) is constant & ((h")(#)(f/*h)).0 = 0.F by
VALUED_0:def 18;
hence (h")(#)(f/*h) is convergent & lim ((h")(#)(f/*h))
= 0.F by NDIFF_1:21;
end;
hence thesis;
end;
end;
definition let F;
mode REST of F is REST-like PartFunc of REAL,the carrier of F;
end;
definition let F;
let IT be Function of REAL,the carrier of F;
attr IT is linear means :Def2:
ex r be Point of F st for p be Real holds IT.p = p*r;
end;
registration let F;
cluster linear Function of REAL,the carrier of F;
existence
proof
deffunc FG(Element of REAL) = $1*(0.F);
consider f be Function of REAL, the carrier of F such that
A1: for x being Element of REAL holds f.x = FG(x) from FUNCT_2:sch 4;
take f;
thus thesis by Def2,A1;
end;
end;
definition let F;
mode LINEAR of F is linear Function of REAL,the carrier of F;
end;
reserve R,R1,R2 for REST of F;
reserve L,L1,L2 for LINEAR of F;
theorem Th3:
L1+L2 is LINEAR of F & L1-L2 is LINEAR of F
proof
consider g1 be Point of F such that
A1: for p be Real holds L1.p = p*g1 by Def2;
consider g2 be Point of F such that
A2: for p be Real holds L2.p = p*g2 by Def2;
A3: L1+L2 is total by VFUNCT_1:38; then
A4: dom (L1+L2) = REAL by FUNCT_2:def 1;
now
let p be Real;
thus (L1+L2).p = (L1+L2)/.p by A4,PARTFUN1:def 8
.= L1/.p + L2/.p by VFUNCT_1:43
.= p*g1 + L2.p by A1
.= p*g1 + p*g2 by A2
.= p*(g1+g2) by RLVECT_1:def 8;
end;
hence L1+L2 is LINEAR of F by A3,Def2;
A5: L1-L2 is total by VFUNCT_1:38; then
A6: dom (L1-L2) = REAL by FUNCT_2:def 1;
now
let p be Real;
thus (L1-L2).p = (L1-L2)/.p by A6,PARTFUN1:def 8
.= L1/.p - L2/.p by VFUNCT_1:43
.= p*g1 - L2.p by A1
.= p*g1 - p*g2 by A2
.= p*(g1-g2) by RLVECT_1:48;
end;
hence thesis by A5,Def2;
end;
theorem Th4:
r(#)L is LINEAR of F
proof
consider g be Point of F such that
A1: for p be Real holds L.p = p*g by Def2;
A2: r(#)L is total by VFUNCT_1:40; then
A3: dom (r(#)L) = REAL by FUNCT_2:def 1;
now
let p be Real;
thus (r(#)L).p =(r(#)L)/.p by A3,PARTFUN1:def 8
.= r*L/.p by VFUNCT_1:45
.= r*(p*g) by A1
.= (r*p)*g by RLVECT_1:def 10
.= p*(r*g) by RLVECT_1:def 10;
end;
hence thesis by A2,Def2;
end;
theorem Th5:
for h1,h2 be PartFunc of REAL, the carrier of F
for seq be Real_Sequence st rng seq c= dom h1 /\ dom h2 holds
(h1+h2)/*seq = h1/*seq+h2/*seq & (h1-h2)/*seq=h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of REAL,the carrier of F;
let seq be Real_Sequence;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2; then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now let n;
A5:seq.n in rng seq by FUNCT_2:6;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:186
.= h1/.(seq.n) + h2/.(seq.n) by A4,A5,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:186,XBOOLE_1:1
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:186,XBOOLE_1:1;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 5;
A6: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n;
A7:seq.n in rng seq by FUNCT_2:6;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A6,FUNCT_2:186
.= h1/.(seq.n) - h2/.(seq.n) by A6,A7,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:186,XBOOLE_1:1
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:186,XBOOLE_1:1;
end;
hence thesis by NORMSP_1:def 6;
end;
theorem Th6:
for h1,h2 be PartFunc of REAL,the carrier of F
for seq be Real_Sequence st h1 is total & h2 is total holds
(h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of REAL,the carrier of F;
let seq be Real_Sequence;
assume h1 is total & h2 is total;
then h1+h2 is total by VFUNCT_1:38;
then dom (h1+h2) = REAL by PARTFUN1:def 4;
then dom h1 /\ dom h2 = REAL by VFUNCT_1:def 1;then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by Th5;
thus thesis by A1,Th5;
end;
theorem Th7:
R1+R2 is REST of F & R1-R2 is REST of F
proof
A1: R1 is total & R2 is total by Def1;
A2: now
let h;
A3: (h")(#)((R1+R2)/*h) = (h")(#)((R1/*h)+(R2/*h)) by A1,Th6
.= ((h")(#)(R1/*h))+((h")(#)(R2/*h)) by NDIFF_1:9;
A4: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def1;
hence (h")(#)((R1+R2)/*h) is convergent by A3,NORMSP_1:34;
lim ((h")(#)(R1/*h)) = 0.F & lim ((h")(#)(R2/*h)) = 0.F by Def1;
hence lim ((h")(#)((R1+R2)/*h)) = 0.F+0.F by A4,A3,NORMSP_1:42
.= 0.F by RLVECT_1:def 7;
end;
R1+R2 is total by A1,VFUNCT_1:38;
hence R1+R2 is REST of F by A2,Def1;
A5: now let h;
A6: (h")(#)((R1-R2)/*h) = (h")(#)((R1/*h)-(R2/*h)) by A1,Th6
.= ((h")(#)(R1/*h))-((h")(#)(R2/*h)) by NDIFF_1:12;
A7: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def1;
hence (h")(#)((R1-R2)/*h) is convergent by A6,NORMSP_1:35;
lim ((h")(#)(R1/*h)) = 0.F & lim ((h")(#)(R2/*h)) = 0.F by Def1;
hence lim ((h")(#)((R1-R2)/*h)) = 0.F-0.F by A7,A6,NORMSP_1:43
.= 0.F by RLVECT_1:26;
end;
R1-R2 is total by A1,VFUNCT_1:38;
hence R1-R2 is REST of F by A5,Def1;
end;
theorem Th8:
r(#)R is REST of F
proof
A1: R is total by Def1; then
A2:r(#)R is total by VFUNCT_1:40;
now let h;
dom R = REAL by A1,FUNCT_2:def 1; then
rng h c= dom R; then
A3: (h")(#)((r(#)R)/*h) = (h")(#)(r*(R/*h)) by NFCONT_3:4
.= r*((h")(#)(R/*h)) by NDIFF_1:10;
A4: (h")(#)(R/*h) is convergent by Def1;
hence (h")(#)((r(#)R)/*h) is convergent by A3,NORMSP_1:37;
lim ((h")(#)(R/*h)) = 0.F by Def1;
hence lim ((h")(#)((r(#)R)/*h)) = r*0.F by A4,A3,NORMSP_1:45
.= 0.F by RLVECT_1:23;
end;
hence thesis by A2,Def1;
end;
definition let F,f;
let x0 be real number;
pred f is_differentiable_in x0 means :Def3:
ex N being Neighbourhood of x0
st N c= dom f & ex L,R st for x st x in N
holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0);
end;
definition
let F,f;
let x0 be real number;
assume
A1: f is_differentiable_in x0;
func diff(f,x0) -> Point of F means :Def4:
ex N being Neighbourhood of x0 st N c= dom f & ex L,R st it=L.1
& for x st x in N holds f/.x-f/.x0 = L.(x-x0) + R/.(x-x0);
existence
proof
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L,R st for x st x in N
holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0) by A1,Def3;
consider L,R such that
A4: for x st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0) by A3;
consider r be Point of F such that
A5: for p be Real holds L.p = p*r by Def2;
take r;
L.1=1*r by A5
.=r by RLVECT_1:def 11;
hence thesis by A2,A4;
end;
uniqueness
proof
let r,s be Point of F;
assume that
A6: ex N being Neighbourhood of x0 st N c= dom f & ex L,R st r=L.1 &
for x be Real st x in N holds f/.x-f/.x0 = L.(x-x0)+R/.(x-x0) and
A7: ex N being Neighbourhood of x0 st N c= dom f & ex L,R st s=L.1 &
for x be Real st x in N holds f/.x-f/.x0 = L.(x-x0) + R/.(x-x0);
consider N being Neighbourhood of x0 such that
N c= dom f and
A8: ex L,R st r=L.1 & for x be Real
st x in N holds f/.x-f/.x0 = L.(x-x0)+R/.(x-x0) by A6;
consider L,R such that
A9: r=L.1 and
A10: for x be Real st x in N holds f/.x-f/.x0 = L.(x-x0) + R/.(x-x0) by A8;
consider r1 be Point of F such that
A11: for p be Real holds L.p = p*r1 by Def2;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A12: ex L,R st s=L.1 & for x be Real st x in N1
holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A7;
consider L1,R1 such that
A13: s =L1.1 and
A14: for x be Real st x in N1
holds f/.x-f/.x0 = L1.(x-x0) + R1/.(x-x0) by A12;
consider p1 be Point of F such that
A15: for p be Real holds L1.p = p*p1 by Def2;
consider N0 be Neighbourhood of x0 such that
A16: N0 c= N & N0 c= N1 by RCOMP_1:38;
consider g be real number such that
A17: 0