let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
let Z be Subset of (product S); :: thesis: for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
let f be PartFunc of (product S),T; :: thesis: for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
let a be Real; :: thesis: for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
let i be set ; :: thesis: ( Z is open & i in dom S & f is_partial_differentiable_on Z,i implies ( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) ) )
assume that
A1: ( Z is open & i in dom S ) and
A2: f is_partial_differentiable_on Z,i ; :: thesis: ( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )
A3: Z c= dom f by A2, NDIFF_5:def 8;
then A4: Z c= dom (a (#) f) by VFUNCT_1:def 4;
for x being Point of (product S) st x in Z holds
(a (#) f) | Z is_partial_differentiable_in x,i

proof

let x be Point of (product S); :: thesis: ( x in Z implies (a (#) f) | Z is_partial_differentiable_in x,i )
assume x in Z ; :: thesis: (a (#) f) | Z is_partial_differentiable_in x,i
then f | Z is_partial_differentiable_in x,i by A2, NDIFF_5:def 8;
then A5: a (#) (f | Z) is_partial_differentiable_in x,i by A1, NDIFF_5:30;
A6: dom (f | Z) = Z by A3, RELAT_1:62;
A7: dom ((a (#) f) | Z) = Z by A4, RELAT_1:62;
for x being Element of (product S) st x in dom ((a (#) f) | Z) holds
((a (#) f) | Z) /. x = a * ((f | Z) /. x)

proof

let x be Element of (product S); :: thesis: ( x in dom ((a (#) f) | Z) implies ((a (#) f) | Z) /. x = a * ((f | Z) /. x) )
assume A8: x in dom ((a (#) f) | Z) ; :: thesis: ((a (#) f) | Z) /. x = a * ((f | Z) /. x)
hence ((a (#) f) | Z) /. x = (a (#) f) /. x by PARTFUN1:80
.= a * (f /. x) by A4, A7, A8, VFUNCT_1:def 4
.= a * ((f | Z) /. x) by A6, A8, PARTFUN1:80 ;
:: thesis: verum

end;

hence (a (#) f) | Z is_partial_differentiable_in x,i by A4, A5, A6, RELAT_1:62, VFUNCT_1:def 4; :: thesis: verum

end;

hence A9: a (#) f is_partial_differentiable_on Z,i by A4, NDIFF_5:def 8; :: thesis: (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i))
set pfg = a (#) (f `partial| (Z,i));
dom (f `partial| (Z,i)) = Z by A2, NDIFF_5:def 9;
then A10: dom (a (#) (f `partial| (Z,i))) = Z by VFUNCT_1:def 4;
for x being Point of (product S) st x in Z holds
(a (#) (f `partial| (Z,i))) /. x = partdiff ((a (#) f),x,i)

proof

let x be Point of (product S); :: thesis: ( x in Z implies (a (#) (f `partial| (Z,i))) /. x = partdiff ((a (#) f),x,i) )
assume A11: x in Z ; :: thesis: (a (#) (f `partial| (Z,i))) /. x = partdiff ((a (#) f),x,i)
then A12: f is_partial_differentiable_in x,i by A1, A2, NDIFF_5:32;
thus (a (#) (f `partial| (Z,i))) /. x = a * ((f `partial| (Z,i)) /. x) by A10, A11, VFUNCT_1:def 4
.= a * (partdiff (f,x,i)) by A2, A11, NDIFF_5:def 9
.= partdiff ((a (#) f),x,i) by A1, A12, NDIFF_5:30 ; :: thesis: verum

end;

hence (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) by A9, A10, NDIFF_5:def 9; :: thesis: verum