let E, F, G be RealNormSpace; :: thesis: for Z being Subset of E
for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) )
let Z be Subset of E; :: thesis: for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) )
let u be PartFunc of E,F; :: thesis: for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) )
let L be Lipschitzian LinearOperator of F,G; :: thesis: for i being Nat st u is_differentiable_on i,Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) )
defpred S₁[ Nat] means ( u is_differentiable_on $1,Z implies ( L * u is_differentiable_on $1,Z & diff ((L * u),$1,Z) = (LTRN ($1,L,E)) * (diff (u,$1,Z)) ) );
A1: S₁[ 0 ]

proof

assume A2: u is_differentiable_on 0 ,Z ; :: thesis: ( L * u is_differentiable_on 0 ,Z & diff ((L * u),0,Z) = (LTRN (0,L,E)) * (diff (u,0,Z)) )
A3: dom L = [#] F by FUNCT_2:def 1;
then A4: rng u c= dom L ;
then A5: Z c= dom (L * u) by A2, RELAT_1:27;
A6: dom (u | Z) = Z by A2, RELAT_1:62;
rng (u | Z) c= dom L by A3;
then A7: dom (L * (u | Z)) = dom (u | Z) by RELAT_1:27
.= Z by A2, RELAT_1:62 ;

A8: now :: thesis: for x being object st x in dom ((L * u) | Z) holds
((L * u) | Z) . x = (L * (u | Z)) . x

let x be object ; :: thesis: ( x in dom ((L * u) | Z) implies ((L * u) | Z) . x = (L * (u | Z)) . x )
assume A9: x in dom ((L * u) | Z) ; :: thesis: ((L * u) | Z) . x = (L * (u | Z)) . x
then A10: x in Z ;
thus ((L * u) | Z) . x = (L * u) . x by A9, FUNCT_1:47
.= L . (u . x) by A2, A10, FUNCT_1:13
.= L . ((u | Z) . x) by A6, A9, FUNCT_1:47
.= (L * (u | Z)) . x by A6, A9, FUNCT_1:13 ; :: thesis: verum

end;

thus L * u is_differentiable_on 0 ,Z by A2, A4, RELAT_1:27; :: thesis: diff ((L * u),0,Z) = (LTRN (0,L,E)) * (diff (u,0,Z))
A11: diff ((L * u),0,Z) = (L * u) | Z by NDIFF_6:11;
(LTRN (0,L,E)) * (diff (u,0,Z)) = L * (diff (u,0,Z)) by Th22
.= L * (u | Z) by NDIFF_6:11 ;
hence diff ((L * u),0,Z) = (LTRN (0,L,E)) * (diff (u,0,Z)) by A5, A7, A8, A11, RELAT_1:62, FUNCT_1:2; :: thesis: verum

end;

A12: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A13: S₁[i] ; :: thesis: S₁[i + 1]
assume A14: u is_differentiable_on i + 1,Z ; :: thesis: ( L * u is_differentiable_on i + 1,Z & diff ((L * u),(i + 1),Z) = (LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z)) )
A15: 0 + i <= 1 + i by XREAL_1:7;
then A16: ( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) ) by A13, A14, NDIFF_6:17;
A17: diff (u,i,Z) is_differentiable_on Z by A14, NDIFF_6:14;
then A18: ( (LTRN (i,L,E)) * (diff (u,i,Z)) is_differentiable_on Z & ( for x being Point of E st x in Z holds
(((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) /. x = (LTRN (i,L,E)) * (((diff (u,i,Z)) `| Z) /. x) ) ) by Th21;
for k being Nat st k <= (i + 1) - 1 holds
diff ((L * u),k,Z) is_differentiable_on Z

proof

let k be Nat; :: thesis: ( k <= (i + 1) - 1 implies diff ((L * u),k,Z) is_differentiable_on Z )
assume A19: k <= (i + 1) - 1 ; :: thesis: diff ((L * u),k,Z) is_differentiable_on Z

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: diff ((L * u),k,Z) is_differentiable_on Z

hence diff ((L * u),k,Z) is_differentiable_on Z by A13, A14, A15, A17, Th21, NDIFF_6:17; :: thesis: verum

end;

suppose k <> i ; :: thesis: diff ((L * u),k,Z) is_differentiable_on Z

then k < i by A19, XXREAL_0:1;
then k + 1 <= i by NAT_1:13;
then (k + 1) - 1 <= i - 1 by XREAL_1:13;
hence diff ((L * u),k,Z) is_differentiable_on Z by A13, A14, A15, NDIFF_6:14, NDIFF_6:17; :: thesis: verum

end;

end;

end;

hence L * u is_differentiable_on i + 1,Z by A16, NDIFF_6:14; :: thesis: diff ((L * u),(i + 1),Z) = (LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))
A20: (diff (u,i,Z)) `| Z = diff (u,(i + 1),Z) by NDIFF_6:13;
A21: dom (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) = Z by A18, NDIFF_1:def 9;
A22: dom ((diff (u,i,Z)) `| Z) = Z by A17, NDIFF_1:def 9;
A23: dom (diff (u,(i + 1),Z)) = Z by A17, A20, NDIFF_1:def 9;
dom (LTRN ((i + 1),L,E)) = the carrier of (diff_SP ((i + 1),E,F)) by FUNCT_2:def 1;
then rng (diff (u,(i + 1),Z)) c= dom (LTRN ((i + 1),L,E)) ;
then A24: dom ((LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))) = Z by A23, RELAT_1:27;

A25: now :: thesis: for x0 being object st x0 in dom (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) holds
(((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) . x0 = ((LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))) . x0

let x0 be object ; :: thesis: ( x0 in dom (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) implies (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) . x0 = ((LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))) . x0 )
assume A26: x0 in dom (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) ; :: thesis: (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) . x0 = ((LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))) . x0
then reconsider x = x0 as Point of E ;
reconsider V = ((diff (u,i,Z)) `| Z) /. x as Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) by LOPBAN_1:def 9;
A27: ((diff (u,i,Z)) `| Z) /. x = ((diff (u,i,Z)) `| Z) . x by A21, A22, A26, PARTFUN1:def 6
.= (diff (u,(i + 1),Z)) . x by NDIFF_6:13 ;
thus (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) . x0 = (((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z) /. x by A26, PARTFUN1:def 6
.= (LTRN (i,L,E)) * (((diff (u,i,Z)) `| Z) /. x) by A17, A21, A26, Th21
.= (LTRN ((i + 1),L,E)) . V by Th22
.= ((LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z))) . x0 by A20, A21, A22, A26, A27, FUNCT_1:13 ; :: thesis: verum

end;

((LTRN (i,L,E)) * (diff (u,i,Z))) `| Z = diff ((L * u),(i + 1),Z) by A13, A14, A15, NDIFF_6:13, NDIFF_6:17;
hence diff ((L * u),(i + 1),Z) = (LTRN ((i + 1),L,E)) * (diff (u,(i + 1),Z)) by A25, FUNCT_1:2, A21, A24; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A12);
hence for i being Nat st u is_differentiable_on i,Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) ) ; :: thesis: verum