let S, T be RealNormSpace; ( (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; ( (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; (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; verum