let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S holds
( (diff (f,Z)) . 0 = f | Z & (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S holds
( (diff (f,Z)) . 0 = f | Z & (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )
let Z be Subset of S; :: thesis: ( (diff (f,Z)) . 0 = f | Z & (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )
thus A1: (diff (f,Z)) . 0 = f | Z by Def5; :: thesis: ( (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )
A2: diff_SP (0,S,T) = T by Th7;
then A3: modetrans (((diff (f,Z)) . 0),S,(diff_SP (0,S,T))) = f | Z by A1, Def4;
(diff (f,Z)) . 1 = (diff (f,Z)) . (0 + 1) ;
hence A4: (diff (f,Z)) . 1 = (f | Z) `| Z by A3, A2, Def5; :: thesis: (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z
A5: diff_SP (1,S,T) = R_NormSpace_of_BoundedLinearOperators (S,T) by Th7;
then A6: modetrans (((diff (f,Z)) . 1),S,(diff_SP (1,S,T))) = (f | Z) `| Z by A4, Def4;
(diff (f,Z)) . 2 = (diff (f,Z)) . (1 + 1) ;
hence (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z by A5, A6, Def5; :: thesis: verum