reconsider x1 = 0. (REAL-NS n) as Element of REAL n by Def4;
( |.x1.| = 0 iff x1 = 0* n ) by EUCLID:7, EUCLID:8;
hence ||.(0. (REAL-NS n)).|| = 0 by Def4, Th1; :: according to NORMSP_0:def 6 :: thesis: ( REAL-NS n is discerning & REAL-NS n is RealNormSpace-like & REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
for x, y being Point of (REAL-NS n)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

proof

let x, y be Point of (REAL-NS n); :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
thus ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

proof

reconsider x1 = x as Element of REAL n by Def4;
( |.x1.| = 0 iff x1 = 0* n ) by EUCLID:7, EUCLID:8;
hence ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) by Def4, Th1; :: thesis: verum

end;

thus ||.(a * x).|| = |.a.| * ||.x.|| :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

proof

reconsider x1 = x as Element of REAL n by Def4;
thus ||.(a * x).|| = |.(a * x1).| by Th1, Th3
.= |.a.| * |.x1.| by EUCLID:11
.= |.a.| * ||.x.|| by Th1 ; :: thesis: verum

end;

thus ||.(x + y).|| <= ||.x.|| + ||.y.|| :: thesis: verum

proof

reconsider x1 = x, y1 = y as Element of REAL n by Def4;
|.(x1 + y1).| <= |.x1.| + |.y1.| by EUCLID:12;
then A1: |.(x1 + y1).| <= ||.x.|| + |.y1.| by Th1;
||.(x + y).|| = |.(x1 + y1).| by Th1, Th2;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, Th1; :: thesis: verum

end;

end;

hence ( REAL-NS n is discerning & REAL-NS n is RealNormSpace-like ) by NORMSP_1:def 1; :: thesis: ( REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
A2: for a, b being Real
for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be Real; :: thesis: for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real ;
let v be VECTOR of (REAL-NS n); :: thesis: (a + b) * v = (a * v) + (b * v)
(a + b) * v = (a * v) + (b * v)

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
A3: ( a * v = a * v1 & b * v = b * v1 ) by Th3;
thus (a + b) * v = (Euclid_mult n) . ((a + b),v) by Def4
.= (a + b) * v2 by Def2
.= (a * v2) + (b * v2) by RVSUM_1:50
.= (a * v) + (b * v) by A3, Th2 ; :: thesis: verum

end;

hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

A4: for a being Real
for v, w being VECTOR of (REAL-NS n) holds a * (v + w) = (a * v) + (a * w)

proof

let a be Real; :: thesis: for v, w being VECTOR of (REAL-NS n) holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real ;
let v, w be VECTOR of (REAL-NS n); :: thesis: a * (v + w) = (a * v) + (a * w)
a * (v + w) = (a * v) + (a * w)

proof

reconsider v1 = v, w1 = w as Element of REAL n by Def4;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;
A5: ( a * v = a * v1 & a * w = a * w1 ) by Th3;
thus a * (v + w) = (Euclid_mult n) . (a,(v + w)) by Def4
.= (Euclid_mult n) . (a,(v1 + w1)) by Th2
.= a * (v2 + w2) by Def2
.= (a * v2) + (a * w2) by RVSUM_1:51
.= (a * v) + (a * w) by A5, Th2 ; :: thesis: verum

end;

hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

A6: for a, b being Real
for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)

proof

let a, b be Real; :: thesis: for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real ;
let v be VECTOR of (REAL-NS n); :: thesis: (a * b) * v = a * (b * v)
(a * b) * v = a * (b * v)

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
A7: b * v = b * v1 by Th3;
(a * b) * v = (Euclid_mult n) . ((a * b),v) by Def4
.= (a * b) * v1 by Def2
.= a * (b * v2) by RVSUM_1:49 ;
hence (a * b) * v = a * (b * v) by A7, Th3; :: thesis: verum

end;

hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

for v being VECTOR of (REAL-NS n) holds 1 * v = v

proof

let v be VECTOR of (REAL-NS n); :: thesis: 1 * v = v
thus 1 * v = v :: thesis: verum

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
thus 1 * v = (Euclid_mult n) . (1,v) by Def4
.= 1 * v2 by Def2
.= v by RVSUM_1:52 ; :: thesis: verum

end;

end;

hence ( REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital ) by A4, A2, A6; :: thesis: ( REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
for v, w being VECTOR of (REAL-NS n) holds v + w = w + v

proof

let v, w be VECTOR of (REAL-NS n); :: thesis: v + w = w + v
thus v + w = w + v :: thesis: verum

proof

reconsider v1 = v, w1 = w as Element of REAL n by Def4;
thus v + w = (Euclid_add n) . (v,w) by Def4
.= (Euclid_add n) . (w1,v1) by BINOP_1:def 2
.= w + v by Def4 ; :: thesis: verum

end;

end;

hence REAL-NS n is Abelian ; :: thesis: ( REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
for u, v, w being VECTOR of (REAL-NS n) holds (u + v) + w = u + (v + w)

proof

let u, v, w be VECTOR of (REAL-NS n); :: thesis: (u + v) + w = u + (v + w)
thus (u + v) + w = u + (v + w) :: thesis: verum

proof

reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def4;
A8: v + w = v1 + w1 by Th2;
thus (u + v) + w = (Euclid_add n) . (( the addF of (REAL-NS n) . (u,v)),w) by Def4
.= (Euclid_add n) . (((Euclid_add n) . (u1,v1)),w1) by Def4
.= (Euclid_add n) . (u1,((Euclid_add n) . (v1,w1))) by BINOP_1:def 3
.= (Euclid_add n) . (u1,(v1 + w1)) by Def1
.= u1 + (v1 + w1) by Def1
.= u + (v + w) by A8, Th2 ; :: thesis: verum

end;

end;

hence REAL-NS n is add-associative ; :: thesis: ( REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
for v being VECTOR of (REAL-NS n) holds v + (0. (REAL-NS n)) = v

proof

let v be VECTOR of (REAL-NS n); :: thesis: v + (0. (REAL-NS n)) = v
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
reconsider zz = n |-> (In (0,REAL)) as Element of n -tuples_on REAL ;
0. (REAL-NS n) = 0* n by Def4;
hence v + (0. (REAL-NS n)) = v1 + (0* n) by Th2
.= v2 + zz by EUCLID:def 4
.= v by RVSUM_1:16 ;
:: thesis: verum

end;

hence REAL-NS n is right_zeroed ; :: thesis: REAL-NS n is right_complementable
REAL-NS n is right_complementable

proof

let v be VECTOR of (REAL-NS n); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
thus ex w being VECTOR of (REAL-NS n) st v + w = 0. (REAL-NS n) :: according to ALGSTR_0:def 11 :: thesis: verum

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
A9: 0. (REAL-NS n) = 0* n by Def4
.= n |-> 0 by EUCLID:def 4 ;
reconsider w = - v1 as VECTOR of (REAL-NS n) by Def4;
take w ; :: thesis: v + w = 0. (REAL-NS n)
thus v + w = v2 + (- v2) by Th2
.= 0. (REAL-NS n) by A9, RVSUM_1:22 ; :: thesis: verum

end;

end;

hence REAL-NS n is right_complementable ; :: thesis: verum