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

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