let m be non zero Nat; for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)
let f be PartFunc of (REAL m),REAL; for x being Element of REAL m st f is_differentiable_in x holds
for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)
let x be Element of REAL m; ( f is_differentiable_in x implies for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v) )
assume A1:
f is_differentiable_in x
; for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)
let u, v be Element of REAL m; (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)
A3:
diff (f,x) = (proj (1,1)) * (diff ((<>* f),x))
by PDIFF_7:def 2;
<>* f is_differentiable_in x
by A1, PDIFF_7:def 1;
then consider g being PartFunc of (REAL-NS m),(REAL-NS 1), y being Point of (REAL-NS m) such that
A4:
( <>* f = g & x = y & diff ((<>* f),x) = diff (g,y) )
by PDIFF_1:def 8;
reconsider DF = diff (g,y) as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
A5:
DF is additive
;
A6: dom (diff ((<>* f),x)) =
dom DF
by A4
.=
the carrier of (REAL-NS m)
by FUNCT_2:def 1
;
A7:
the carrier of (REAL-NS m) = REAL m
by REAL_NS1:def 4;
reconsider u1 = u, v1 = v as Point of (REAL-NS m) by REAL_NS1:def 4;
thus (diff (f,x)) . (u + v) =
((proj (1,1)) * (diff ((<>* f),x))) . (u + v)
by PDIFF_7:def 2
.=
(proj (1,1)) . ((diff ((<>* f),x)) . (u + v))
by A6, A7, FUNCT_1:13
.=
(proj (1,1)) . (DF . (u1 + v1))
by A4, REAL_NS1:2
.=
(proj (1,1)) . ((DF . u1) + (DF . v1))
by A5
.=
((proj (1,1)) . (DF . u1)) + ((proj (1,1)) . (DF . v1))
by PDIFF_1:4
.=
(((proj (1,1)) * (diff ((<>* f),x))) . u) + ((proj (1,1)) . ((diff ((<>* f),x)) . v))
by A4, A6, FUNCT_1:13
.=
((diff (f,x)) . u) + ((diff (f,x)) . v)
by A3, A6, A7, FUNCT_1:13
; verum