let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( ( ||.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; :: thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus 0 <= ||.x.|| by A2; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus ||.(x + y).|| <= ||.x.|| + ||.y.|| by A2, A3, A4, NORMSP_1:def 1; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||
thus ||.(a * x).|| = |.a.| * ||.x.|| by A2, A5, NORMSP_1:def 1; :: thesis: verum