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