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

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