let S, T be RealNormSpace; :: thesis: ( (diff_SP (S,T)) . 0 = T & (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,T) & (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T))) )
thus A1: (diff_SP (S,T)) . 0 = T by Def2; :: thesis: ( (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,T) & (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T))) )
(diff_SP (S,T)) . 1 = (diff_SP (S,T)) . (0 + 1) ;
then (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,(modetrans ((diff_SP (S,T)) . 0))) by Def2;
hence A2: (diff_SP (S,T)) . 1 = R_NormSpace_of_BoundedLinearOperators (S,T) by A1, Def1; :: thesis: (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T)))
(diff_SP (S,T)) . 2 = (diff_SP (S,T)) . (1 + 1) ;
then (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(modetrans ((diff_SP (S,T)) . 1))) by Def2;
hence (diff_SP (S,T)) . 2 = R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,T))) by A2, Def1; :: thesis: verum