let S, T be RealNormSpace; :: thesis: for i being Nat ex H being RealNormSpace st
( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) )
let i be Nat; :: thesis: ex H being RealNormSpace st
( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) )
take H = modetrans ((diff_SP (S,T)) . i); :: thesis: ( H = (diff_SP (S,T)) . i & (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) )
thus H = (diff_SP (S,T)) . i by Def1, Th8; :: thesis: (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H)
thus (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) by Def2; :: thesis: verum