let X, Y be RealNormSpace; for T being LinearOperator of X,Y
for x, y being Point of (graphNSP T)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let T be LinearOperator of X,Y; for x, y being Point of (graphNSP T)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let x, y be Point of (graphNSP T); for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let a be Real; ( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
( x in graph T & y in graph T )
;
then reconsider x1 = x, y1 = y as Point of [:X,Y:] ;
set W = graphNSP T;
set V = [:X,Y:];
A1:
graphNSP T is Subspace of [:X,Y:]
by Th9;
A2:
||.x.|| = ||.x1.||
by FUNCT_1:49;
A3:
||.y.|| = ||.y1.||
by FUNCT_1:49;
x + y = x1 + y1
by A1, RLSUB_1:13;
then A4:
||.(x + y).|| = ||.(x1 + y1).||
by FUNCT_1:49;
a * x = a * x1
by A1, RLSUB_1:14;
then A5:
||.(a * x).|| = ||.(a * x1).||
by FUNCT_1:49;
A6:
0. [:X,Y:] = 0. (graphNSP T)
by A1, RLSUB_1:11;
( ||.x.|| = 0 iff ||.x1.|| = 0 )
by FUNCT_1:49;
hence
( ||.x.|| = 0 iff x = 0. (graphNSP T) )
by A6, NORMSP_0:def 5; ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus
0 <= ||.x.||
by A2; ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus
||.(x + y).|| <= ||.x.|| + ||.y.||
by A2, A3, A4, NORMSP_1:def 1; ||.(a * x).|| = |.a.| * ||.x.||
thus
||.(a * x).|| = |.a.| * ||.x.||
by A2, A5, NORMSP_1:def 1; verum