:: deftheorem defines graphNrm LOPBAN_7:def 2 :
for X, Y being RealNormSpace
for T being LinearOperator of X,Y holds graphNrm T = the normF of [:X,Y:] | (graph T);