set N = the normF of V | the carrier of W;
dom the normF of V = the carrier of V by FUNCT_2:def 1;
then the carrier of W c= dom the normF of V by RLSUB_1:def 2;
then ( dom ( the normF of V | the carrier of W) = the carrier of W & rng ( the normF of V | the carrier of W) c= REAL ) by RELAT_1:62;
then reconsider N = the normF of V | the carrier of W as Function of the carrier of W,REAL by FUNCT_2:2;
reconsider X = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W,N #) as non empty NORMSTR ;
A1: for a being Real
for v being Element of X
for v1 being Element of W st v = v1 holds
a * v = a * v1

let a be Real; :: thesis:
let v be Element of X; :: thesis:
let v1 be Element of W; :: thesis:
assume A2: v = v1 ; :: thesis:
thus a * v = the Mult of X . (a,v) by RLVECT_1:def 1
.= a * v1 by RLVECT_1:def 1, A2 ; :: thesis:

end;

let v, w be Element of X; :: thesis:
reconsider v1 = v, w1 = w as Element of W ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis:

end;

let u, v, w be Element of X; :: thesis:
reconsider u1 = u, v1 = v, w1 = w as Element of W ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis:

end;

let v be Element of X; :: thesis:
reconsider v1 = v as Element of W ;
thus v + (0. X) = v1 + (0. W)
.= v ; :: thesis:

end;

A6: for a being Real
for v, w being VECTOR of X holds a * (v + w) = (a * v) + (a * w)

let a be Real; :: thesis:
let v, w be VECTOR of X; :: thesis:
reconsider v1 = v, w1 = w as VECTOR of W ;
A7: a * w1 = a * w by A1;
thus a * (v + w) = a * (v1 + w1) by A1
.= (a * v1) + (a * w1) by RLVECT_1:def 5
.= (a * v) + (a * w) by A1, A7 ; :: thesis:

end;

A8: for a, b being Real
for v being VECTOR of X holds (a + b) * v = (a * v) + (b * v)

let a, b be Real; :: thesis:
let v be VECTOR of X; :: thesis:
reconsider v1 = v as VECTOR of W ;
A9: ( a * v1 = a * v & b * v1 = b * v ) by A1;
thus (a + b) * v = (a + b) * v1 by A1
.= (a * v1) + (b * v1) by RLVECT_1:def 6
.= (a * v) + (b * v) by A9 ; :: thesis:

end;

A10: for a, b being Real
for v being VECTOR of X holds (a * b) * v = a * (b * v)

let a, b be Real; :: thesis:
let v be VECTOR of X; :: thesis:
reconsider v1 = v as VECTOR of W ;
A11: b * v1 = b * v by A1;
thus (a * b) * v = (a * b) * v1 by A1
.= a * (b * v1) by RLVECT_1:def 7
.= a * (b * v) by A11, A1 ; :: thesis:

end;

let v be VECTOR of X; :: thesis:
reconsider v1 = v as VECTOR of W ;
thus 1 * v = 1 * v1 by A1
.= v by RLVECT_1:def 8 ; :: thesis:

end;

let x be Element of X; :: thesis:
the carrier of W c= the carrier of V by RLSUB_1:def 2;
then reconsider x1 = x as Element of V ;
assume ||.x.|| = 0 ; :: thesis:
then ||.x1.|| = 0 by FUNCT_1:49;
then x1 = 0. V by NORMSP_0:def 5;
hence x = 0. W by RLSUB_1:def 2
.= 0. X ;
:: thesis:

end;

0. X = 0. W
.= 0. V by RLSUB_1:11 ;
then A15: ||.(0. X).|| = ||.(0. V).|| by FUNCT_1:49
.= 0 ;
A16: for x, y being Point of X
for a being Real holds
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let x, y be Point of X; :: thesis:
let a be Real; :: thesis:
reconsider x2 = x, y2 = y as Element of W ;
the carrier of W c= the carrier of V by RLSUB_1:def 2;
then reconsider x1 = x, y1 = y as Element of V ;
A17P: a * x = a * x2 by A1
.= a * x1 by RLSUB_1:14 ;
||.(a * x1).|| = |.a.| * ||.x1.|| by NORMSP_1:def 1;
then ||.(a * x1).|| = |.a.| * ||.x.|| by FUNCT_1:49;
hence ||.(a * x).|| = |.a.| * ||.x.|| by A17P, FUNCT_1:49; :: thesis:
A18P: x + y = x2 + y2
.= x1 + y1 by RLSUB_1:13 ;
||.(x1 + y1).|| <= ||.x1.|| + ||.y1.|| by NORMSP_1:def 1;
then ||.(x1 + y1).|| <= ||.x.|| + ||.y1.|| by FUNCT_1:49;
then ||.(x1 + y1).|| <= ||.x.|| + ||.y.|| by FUNCT_1:49;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A18P, FUNCT_1:49; :: thesis:

end;

let x be Point of X; :: thesis:
reconsider x1 = x as VECTOR of W ;
consider y1 being Element of W such that
A20: x1 + y1 = 0. W by ALGSTR_0:def 11, ALGSTR_0:def 16;
reconsider y = y1 as Element of X ;
x + y = 0. X by A20;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis:

end;