let X, Y be RealNormSpace; :: thesis: for T being LinearOperator of X,Y holds graphNSP T is Subspace of [:X,Y:]
let T be LinearOperator of X,Y; :: thesis: graphNSP T is Subspace of [:X,Y:]
set l = graphNSP T;
reconsider W = RLSStruct(# the carrier of (graphNSP T), the ZeroF of (graphNSP T), the addF of (graphNSP T), the Mult of (graphNSP T) #) as Subspace of [:X,Y:] by RSSPACE:11;
A1: 0. (graphNSP T) = 0. W
.= 0. [:X,Y:] by RLSUB_1:def 2 ;
A2: the addF of (graphNSP T) = the addF of [:X,Y:] || the carrier of W by RLSUB_1:def 2
.= the addF of [:X,Y:] || the carrier of (graphNSP T) ;
the Mult of (graphNSP T) = the Mult of [:X,Y:] | [:REAL, the carrier of W:] by RLSUB_1:def 2
.= the Mult of [:X,Y:] | [:REAL, the carrier of (graphNSP T):] ;
hence graphNSP T is Subspace of [:X,Y:] by A1, A2, RLSUB_1:def 2; :: thesis: verum