let S be RealNormSpace-Sequence; :: thesis:
let T be RealNormSpace; :: thesis:
let Z be Subset of (product S); :: thesis:
let I be non empty FinSequence of dom S; :: thesis:
let f be PartFunc of (product S),T; :: thesis:
let a be Real; :: thesis:
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I ; :: thesis:
1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25;
then A4: I . 1 in rng I by FUNCT_1:3;
A6: f `partial| (Z,(I . 1)) = PartDiffSeq (f,Z,I,1) by Th13;
A7: Partdiff_SP (S,T,I,1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) by Th12;
A8: PartDiffSeq ((a (#) f),Z,I,1) = (a (#) f) `partial| (Z,(I . 1)) by Th13
.= a (#) (PartDiffSeq (f,Z,I,1)) by A1, A2, A4, A6, A7, Th27 ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 < len I implies ( PartDiffSeq ((a (#) f),Z,I,$1) is_partial_differentiable_on Z,I . ($1 + 1) & PartDiffSeq ((a (#) f),Z,I,($1 + 1)) = a (#) (PartDiffSeq (f,Z,I,($1 + 1))) ) );
A9: S₁[ 0 ] ;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A11: S₁[k] ; :: thesis:
assume A12: ( 1 <= k + 1 & k + 1 < len I ) ; :: thesis:
then A13: PartDiffSeq (f,Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A2;
( 1 <= (k + 1) + 1 & (k + 1) + 1 <= len I ) by A12, NAT_1:13;
then (k + 1) + 1 in dom I by FINSEQ_3:25;
then A14: I . ((k + 1) + 1) in rng I by FUNCT_1:3;
then A15: ( a (#) (PartDiffSeq (f,Z,I,(k + 1))) is_partial_differentiable_on Z,I . ((k + 1) + 1) & (a (#) (PartDiffSeq (f,Z,I,(k + 1)))) `partial| (Z,(I . ((k + 1) + 1))) = a (#) ((PartDiffSeq (f,Z,I,(k + 1))) `partial| (Z,(I . ((k + 1) + 1)))) ) by A1, A13, Th27;
A16: Partdiff_SP (S,T,I,((k + 1) + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . ((k + 1) + 1)),(dom S)))),(Partdiff_SP (S,T,I,(k + 1)))) by A12, Th12;
A18: (a (#) (PartDiffSeq (f,Z,I,(k + 1)))) `partial| (Z,(I . ((k + 1) + 1))) = a (#) (PartDiffSeq (f,Z,I,((k + 1) + 1))) by A12, A15, A16, Th13;

suppose A19: k = 0 ; :: thesis:

hence PartDiffSeq ((a (#) f),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A1, A8, A13, A14, Th27; :: thesis:
thus PartDiffSeq ((a (#) f),Z,I,((k + 1) + 1)) = a (#) (PartDiffSeq (f,Z,I,((k + 1) + 1))) by A8, A12, A18, A19, Th13; :: thesis:

end;

suppose A20: k <> 0 ; :: thesis:

hence PartDiffSeq ((a (#) f),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A1, A11, A12, A13, A14, Th27, NAT_1:13, NAT_1:14; :: thesis:
thus PartDiffSeq ((a (#) f),Z,I,((k + 1) + 1)) = a (#) (PartDiffSeq (f,Z,I,((k + 1) + 1))) by A11, A12, A18, A20, Th13, NAT_1:13, NAT_1:14; :: thesis:

end;

end;

end;

A22: for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10);
hence a (#) f is_partial_differentiable_on Z,I by A1, A2, A4, Th27; :: thesis:
thus for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((a (#) f),Z,I,i) = a (#) (PartDiffSeq (f,Z,I,i)) :: thesis:

let i be Nat; :: thesis:
assume A23: ( 1 <= i & i <= len I ) ; :: thesis:

suppose i = 1 ; :: thesis:

hence PartDiffSeq ((a (#) f),Z,I,i) = a (#) (PartDiffSeq (f,Z,I,i)) by A8; :: thesis:

end;

suppose i <> 1 ; :: thesis:

then 1 < i by XXREAL_0:1, A23;
then 1 + 1 <= i by NAT_1:13;
then A24: 2 - 1 <= i - 1 by XREAL_1:9;
then i - 1 in NAT by INT_1:3;
then reconsider j = i - 1 as Nat ;
j < j + 1 by NAT_1:16;
then j < len I by A23, XXREAL_0:2;
then PartDiffSeq ((a (#) f),Z,I,(j + 1)) = a (#) (PartDiffSeq (f,Z,I,(j + 1))) by A22, A24;
hence PartDiffSeq ((a (#) f),Z,I,i) = a (#) (PartDiffSeq (f,Z,I,i)) ; :: thesis:

end;

end;

end;