let X, Y, W be RealNormSpace; :: thesis: for z being Point of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds
( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )
let z be Point of [:X,Y:]; :: thesis: for r being Real
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds
( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )
let r be Real; :: thesis: for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds
( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )
let f be PartFunc of [:X,Y:],W; :: thesis: ( f is_partial_differentiable_in`1 z implies ( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) ) )
assume A1: f is_partial_differentiable_in`1 z ; :: thesis: ( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )
dom <*X,Y*> = Seg (len <*X,Y*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ;
then D2: 1 in dom <*X,Y*> ;
then In (1,(dom <*X,Y*>)) = 1 by SUBSET_1:def 8;
then BX1: <*X,Y*> . (In (1,(dom <*X,Y*>))) = X ;
P1: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 by LM200, A1;
P3: partdiff`1 ((r (#) f),z) = partdiff (((r (#) f) * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) by LM210;
P4: partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) by LM210;
P6: (r (#) f) * ((IsoCPNrSP (X,Y)) ") = r (#) (f * ((IsoCPNrSP (X,Y)) ")) by Th27;
hence r (#) f is_partial_differentiable_in`1 z by D2, P1, LM200, NDIFF_5:30; :: thesis: partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z))
thus partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) by BX1, D2, P1, P3, P4, P6, NDIFF_5:30; :: thesis: verum