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