now :: thesis: for x, y, z being Point of (REAL-US n)

for a being Real holds

( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

hence
REAL-US n is RealUnitarySpace-like
; :: thesis: ( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )for a being Real holds

( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

let x, y, z be Point of (REAL-US n); :: thesis: for a being Real holds

( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

let a be Real; :: thesis: ( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

reconsider x1 = x, y1 = y, z1 = z as Element of REAL n by Def6;

reconsider x2 = x1, y2 = y1, z2 = z1 as Element of n -tuples_on REAL by EUCLID:def 1;

A1: ( len x2 = n & len y2 = n ) by CARD_1:def 7;

A2: for k being Nat st k in dom (mlt (x1,x1)) holds

0 <= (mlt (x1,x1)) . k

.= Sum (mlt (x1,x1)) by Def5 ;

hence 0 <= x .|. x by A2, RVSUM_1:84; :: thesis: ( ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus ( x .|. x = 0 iff x = 0. (REAL-US n) ) :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus x .|. y = (Euclid_scalar n) . (x,y) by Def6

.= Sum (mlt (y1,x1)) by Def5

.= (Euclid_scalar n) . (y,x) by Def5

.= y .|. x by Def6 ; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

A9: x .|. z = (Euclid_scalar n) . (x,z) by Def6

.= Sum (mlt (x1,z1)) by Def5 ;

a * x is Element of REAL n by Def6;

then reconsider ax = a * x as Element of n -tuples_on REAL by EUCLID:def 1;

A10: for k being Nat st k in Seg n holds

ax . k = (a * x1) . k

.= Sum (mlt (y1,z1)) by Def5 ;

thus (x + y) .|. z = (Euclid_scalar n) . ((x + y),z) by Def6

.= (Euclid_scalar n) . (((Euclid_add n) . (x1,y1)),z1) by Def6

.= (Euclid_scalar n) . ((x1 + y1),z1) by Def1

.= Sum (mlt ((x1 + y1),z1)) by Def5

.= Sum ((mlt (x1,z1)) + (mlt (y1,z1))) by A1, A8, RVSUM_1:118

.= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by RVSUM_1:89

.= (x .|. z) + (y .|. z) by A9, A11 ; :: thesis: (a * x) .|. y = a * (x .|. y)

thus (a * x) .|. y = (Euclid_scalar n) . ((a * x),y) by Def6

.= (Euclid_scalar n) . ((a * x1),y1) by A10, FINSEQ_2:119

.= Sum (mlt ((a * x1),y1)) by Def5

.= Sum (a * (mlt (x2,y2))) by RVSUM_1:65

.= a * (Sum (mlt (x2,y2))) by RVSUM_1:87

.= a * ((Euclid_scalar n) . (x1,y1)) by Def5

.= a * (x .|. y) by Def6 ; :: thesis: verum

end;( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

let a be Real; :: thesis: ( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

reconsider x1 = x, y1 = y, z1 = z as Element of REAL n by Def6;

reconsider x2 = x1, y2 = y1, z2 = z1 as Element of n -tuples_on REAL by EUCLID:def 1;

A1: ( len x2 = n & len y2 = n ) by CARD_1:def 7;

A2: for k being Nat st k in dom (mlt (x1,x1)) holds

0 <= (mlt (x1,x1)) . k

proof

A3: x .|. x =
(Euclid_scalar n) . (x,x)
by Def6
let k be Nat; :: thesis: ( k in dom (mlt (x1,x1)) implies 0 <= (mlt (x1,x1)) . k )

assume k in dom (mlt (x1,x1)) ; :: thesis: 0 <= (mlt (x1,x1)) . k

(mlt (x1,x1)) . k = (x1 . k) * (x1 . k) by RVSUM_1:59;

hence 0 <= (mlt (x1,x1)) . k by XREAL_1:63; :: thesis: verum

end;assume k in dom (mlt (x1,x1)) ; :: thesis: 0 <= (mlt (x1,x1)) . k

(mlt (x1,x1)) . k = (x1 . k) * (x1 . k) by RVSUM_1:59;

hence 0 <= (mlt (x1,x1)) . k by XREAL_1:63; :: thesis: verum

.= Sum (mlt (x1,x1)) by Def5 ;

hence 0 <= x .|. x by A2, RVSUM_1:84; :: thesis: ( ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus ( x .|. x = 0 iff x = 0. (REAL-US n) ) :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

proof

assume x = 0. (REAL-US n) ; :: thesis: x .|. x = 0

then x = 0* n by Def6

.= n |-> 0 by EUCLID:def 4 ;

then mlt (x2,x2) = 0 * x2 by RVSUM_1:63

.= n |-> 0 by RVSUM_1:53 ;

hence x .|. x = 0 by A3, RVSUM_1:81; :: thesis: verum

end;

A8:
len z2 = n
by CARD_1:def 7;now :: thesis: ( x .|. x = 0 implies not x <> 0. (REAL-US n) )

hence
( x .|. x = 0 implies x = 0. (REAL-US n) )
; :: thesis: ( x = 0. (REAL-US n) implies x .|. x = 0 )assume that

A4: x .|. x = 0 and

A5: x <> 0. (REAL-US n) ; :: thesis: contradiction

for k being Element of NAT st k in dom x2 holds

x2 . k = 0

then x = 0* n by EUCLID:def 4;

hence contradiction by A5, Def6; :: thesis: verum

end;A4: x .|. x = 0 and

A5: x <> 0. (REAL-US n) ; :: thesis: contradiction

for k being Element of NAT st k in dom x2 holds

x2 . k = 0

proof

then
x1 = n |-> 0
by RFUNCT_4:4;
let k be Element of NAT ; :: thesis: ( k in dom x2 implies x2 . k = 0 )

dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;

then [:(rng x1),(rng x1):] c= dom multreal by ZFMISC_1:96;

then A6: dom (multreal .: (x1,x1)) = (dom x1) /\ (dom x1) by FUNCOP_1:69;

assume k in dom x2 ; :: thesis: x2 . k = 0

then A7: k in dom (mlt (x1,x1)) by A6, RVSUM_1:def 9;

then 0 <= (mlt (x1,x1)) . k by A2;

then (mlt (x1,x1)) . k = 0 by A3, A2, A4, A7, RVSUM_1:85;

then (x1 . k) ^2 = 0 by RVSUM_1:59;

hence x2 . k = 0 by SQUARE_1:12; :: thesis: verum

end;dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;

then [:(rng x1),(rng x1):] c= dom multreal by ZFMISC_1:96;

then A6: dom (multreal .: (x1,x1)) = (dom x1) /\ (dom x1) by FUNCOP_1:69;

assume k in dom x2 ; :: thesis: x2 . k = 0

then A7: k in dom (mlt (x1,x1)) by A6, RVSUM_1:def 9;

then 0 <= (mlt (x1,x1)) . k by A2;

then (mlt (x1,x1)) . k = 0 by A3, A2, A4, A7, RVSUM_1:85;

then (x1 . k) ^2 = 0 by RVSUM_1:59;

hence x2 . k = 0 by SQUARE_1:12; :: thesis: verum

then x = 0* n by EUCLID:def 4;

hence contradiction by A5, Def6; :: thesis: verum

assume x = 0. (REAL-US n) ; :: thesis: x .|. x = 0

then x = 0* n by Def6

.= n |-> 0 by EUCLID:def 4 ;

then mlt (x2,x2) = 0 * x2 by RVSUM_1:63

.= n |-> 0 by RVSUM_1:53 ;

hence x .|. x = 0 by A3, RVSUM_1:81; :: thesis: verum

thus x .|. y = (Euclid_scalar n) . (x,y) by Def6

.= Sum (mlt (y1,x1)) by Def5

.= (Euclid_scalar n) . (y,x) by Def5

.= y .|. x by Def6 ; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

A9: x .|. z = (Euclid_scalar n) . (x,z) by Def6

.= Sum (mlt (x1,z1)) by Def5 ;

a * x is Element of REAL n by Def6;

then reconsider ax = a * x as Element of n -tuples_on REAL by EUCLID:def 1;

A10: for k being Nat st k in Seg n holds

ax . k = (a * x1) . k

proof

A11: y .|. z =
(Euclid_scalar n) . (y,z)
by Def6
reconsider a = a as Real ;

let k be Nat; :: thesis: ( k in Seg n implies ax . k = (a * x1) . k )

assume k in Seg n ; :: thesis: ax . k = (a * x1) . k

a * x = (Euclid_mult n) . (a,x1) by Def6

.= a * x1 by Def2 ;

hence ax . k = (a * x1) . k ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg n implies ax . k = (a * x1) . k )

assume k in Seg n ; :: thesis: ax . k = (a * x1) . k

a * x = (Euclid_mult n) . (a,x1) by Def6

.= a * x1 by Def2 ;

hence ax . k = (a * x1) . k ; :: thesis: verum

.= Sum (mlt (y1,z1)) by Def5 ;

thus (x + y) .|. z = (Euclid_scalar n) . ((x + y),z) by Def6

.= (Euclid_scalar n) . (((Euclid_add n) . (x1,y1)),z1) by Def6

.= (Euclid_scalar n) . ((x1 + y1),z1) by Def1

.= Sum (mlt ((x1 + y1),z1)) by Def5

.= Sum ((mlt (x1,z1)) + (mlt (y1,z1))) by A1, A8, RVSUM_1:118

.= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by RVSUM_1:89

.= (x .|. z) + (y .|. z) by A9, A11 ; :: thesis: (a * x) .|. y = a * (x .|. y)

thus (a * x) .|. y = (Euclid_scalar n) . ((a * x),y) by Def6

.= (Euclid_scalar n) . ((a * x1),y1) by A10, FINSEQ_2:119

.= Sum (mlt ((a * x1),y1)) by Def5

.= Sum (a * (mlt (x2,y2))) by RVSUM_1:65

.= a * (Sum (mlt (x2,y2))) by RVSUM_1:87

.= a * ((Euclid_scalar n) . (x1,y1)) by Def5

.= a * (x .|. y) by Def6 ; :: thesis: verum

A12: for a, b being Real

for v being VECTOR of (REAL-US n) holds (a * b) * v = a * (b * v)

proof

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

let v be VECTOR of (REAL-US n); :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of REAL n by Def6;

reconsider a = a, b = b as Real ;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

b * v is Element of REAL n by Def6;

then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

bv . k = (b * v1) . k

then A13: a * (b * v) = (Euclid_mult n) . (a,(b * v1)) by Def6

.= a * (b * v2) by Def2 ;

(a * b) * v = (Euclid_mult n) . ((a * b),v1) by Def6

.= (a * b) * v2 by Def2

.= a * (b * v2) by RVSUM_1:49 ;

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

end;let v be VECTOR of (REAL-US n); :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of REAL n by Def6;

reconsider a = a, b = b as Real ;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

b * v is Element of REAL n by Def6;

then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

bv . k = (b * v1) . k

proof

then
b * v1 = b * v
by FINSEQ_2:119;
reconsider b = b as Element of REAL by XREAL_0:def 1;

let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )

assume k in Seg n ; :: thesis: bv . k = (b * v1) . k

b * v = (Euclid_mult n) . (b,v1) by Def6

.= b * v1 by Def2 ;

hence bv . k = (b * v1) . k ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )

assume k in Seg n ; :: thesis: bv . k = (b * v1) . k

b * v = (Euclid_mult n) . (b,v1) by Def6

.= b * v1 by Def2 ;

hence bv . k = (b * v1) . k ; :: thesis: verum

then A13: a * (b * v) = (Euclid_mult n) . (a,(b * v1)) by Def6

.= a * (b * v2) by Def2 ;

(a * b) * v = (Euclid_mult n) . ((a * b),v1) by Def6

.= (a * b) * v2 by Def2

.= a * (b * v2) by RVSUM_1:49 ;

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

for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)

proof

A18:
for a, b being Real
let a be Real; :: thesis: for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)

let v, w be VECTOR of (REAL-US n); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of REAL n by Def6;

reconsider a = a as Real ;

reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;

a * v is Element of REAL n by Def6;

then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def 1;

A15: for k being Nat st k in Seg n holds

av . k = (a * v1) . k

then reconsider aw = a * w as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

aw . k = (a * w1) . k

A17: (a * v) + (a * w) = (Euclid_add n) . ((a * v),(a * w)) by Def6

.= (Euclid_add n) . ((a * v1),(a * w1)) by A15, A16, FINSEQ_2:119

.= (a * v2) + (a * w2) by Def1 ;

a * (v + w) = (Euclid_mult n) . (a,(v + w)) by Def6

.= (Euclid_mult n) . (a,((Euclid_add n) . (v1,w1))) by Def6

.= (Euclid_mult n) . (a,(v1 + w1)) by Def1

.= a * (v1 + w1) by Def2

.= (a * v2) + (a * w2) by RVSUM_1:51 ;

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

end;let v, w be VECTOR of (REAL-US n); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of REAL n by Def6;

reconsider a = a as Real ;

reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;

a * v is Element of REAL n by Def6;

then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def 1;

A15: for k being Nat st k in Seg n holds

av . k = (a * v1) . k

proof

a * w is Element of REAL n
by Def6;
let k be Nat; :: thesis: ( k in Seg n implies av . k = (a * v1) . k )

assume k in Seg n ; :: thesis: av . k = (a * v1) . k

a * v = (Euclid_mult n) . (a,v1) by Def6

.= a * v1 by Def2 ;

hence av . k = (a * v1) . k ; :: thesis: verum

end;assume k in Seg n ; :: thesis: av . k = (a * v1) . k

a * v = (Euclid_mult n) . (a,v1) by Def6

.= a * v1 by Def2 ;

hence av . k = (a * v1) . k ; :: thesis: verum

then reconsider aw = a * w as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

aw . k = (a * w1) . k

proof

then A16:
( a * v1 is Element of n -tuples_on REAL & a * w1 = a * w )
by EUCLID:def 1, FINSEQ_2:119;
reconsider a = a as Element of REAL by XREAL_0:def 1;

let k be Nat; :: thesis: ( k in Seg n implies aw . k = (a * w1) . k )

assume k in Seg n ; :: thesis: aw . k = (a * w1) . k

a * w = (Euclid_mult n) . (a,w1) by Def6

.= a * w1 by Def2 ;

hence aw . k = (a * w1) . k ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg n implies aw . k = (a * w1) . k )

assume k in Seg n ; :: thesis: aw . k = (a * w1) . k

a * w = (Euclid_mult n) . (a,w1) by Def6

.= a * w1 by Def2 ;

hence aw . k = (a * w1) . k ; :: thesis: verum

A17: (a * v) + (a * w) = (Euclid_add n) . ((a * v),(a * w)) by Def6

.= (Euclid_add n) . ((a * v1),(a * w1)) by A15, A16, FINSEQ_2:119

.= (a * v2) + (a * w2) by Def1 ;

a * (v + w) = (Euclid_mult n) . (a,(v + w)) by Def6

.= (Euclid_mult n) . (a,((Euclid_add n) . (v1,w1))) by Def6

.= (Euclid_mult n) . (a,(v1 + w1)) by Def1

.= a * (v1 + w1) by Def2

.= (a * v2) + (a * w2) by RVSUM_1:51 ;

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

for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)

proof

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

let v be VECTOR of (REAL-US n); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of REAL n by Def6;

reconsider a = a, b = b as Real ;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

A19: (a + b) * v = (Euclid_mult n) . ((a + b),v1) by Def6

.= (a + b) * v2 by Def2

.= (a * v1) + (b * v1) by RVSUM_1:50 ;

a * v is Element of REAL n by Def6;

then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def 1;

A20: for k being Nat st k in Seg n holds

av . k = (a * v1) . k

then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

bv . k = (b * v1) . k

(a * v) + (b * v) = (Euclid_add n) . ((a * v),(b * v)) by Def6

.= (Euclid_add n) . ((a * v1),(b * v1)) by A20, A21, FINSEQ_2:119

.= (a * v2) + (b * v2) by Def1 ;

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

end;let v be VECTOR of (REAL-US n); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of REAL n by Def6;

reconsider a = a, b = b as Real ;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

A19: (a + b) * v = (Euclid_mult n) . ((a + b),v1) by Def6

.= (a + b) * v2 by Def2

.= (a * v1) + (b * v1) by RVSUM_1:50 ;

a * v is Element of REAL n by Def6;

then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def 1;

A20: for k being Nat st k in Seg n holds

av . k = (a * v1) . k

proof

b * v is Element of REAL n
by Def6;
reconsider a = a as Element of REAL by XREAL_0:def 1;

let k be Nat; :: thesis: ( k in Seg n implies av . k = (a * v1) . k )

assume k in Seg n ; :: thesis: av . k = (a * v1) . k

a * v = (Euclid_mult n) . (a,v1) by Def6

.= a * v1 by Def2 ;

hence av . k = (a * v1) . k ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg n implies av . k = (a * v1) . k )

assume k in Seg n ; :: thesis: av . k = (a * v1) . k

a * v = (Euclid_mult n) . (a,v1) by Def6

.= a * v1 by Def2 ;

hence av . k = (a * v1) . k ; :: thesis: verum

then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;

for k being Nat st k in Seg n holds

bv . k = (b * v1) . k

proof

then A21:
( a * v1 is Element of n -tuples_on REAL & b * v1 = b * v )
by EUCLID:def 1, FINSEQ_2:119;
reconsider b = b as Element of REAL by XREAL_0:def 1;

let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )

assume k in Seg n ; :: thesis: bv . k = (b * v1) . k

b * v = (Euclid_mult n) . (b,v1) by Def6

.= b * v1 by Def2 ;

hence bv . k = (b * v1) . k ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )

assume k in Seg n ; :: thesis: bv . k = (b * v1) . k

b * v = (Euclid_mult n) . (b,v1) by Def6

.= b * v1 by Def2 ;

hence bv . k = (b * v1) . k ; :: thesis: verum

(a * v) + (b * v) = (Euclid_add n) . ((a * v),(b * v)) by Def6

.= (Euclid_add n) . ((a * v1),(b * v1)) by A20, A21, FINSEQ_2:119

.= (a * v2) + (b * v2) by Def1 ;

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

proof

hence
( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital )
by A14, A18, A12; :: thesis: ( REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
let v be VECTOR of (REAL-US n); :: thesis: 1 * v = v

reconsider v1 = v as Element of REAL n by Def6;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

1 * v = (Euclid_mult n) . (1,v1) by Def6

.= 1 * v2 by Def2

.= v2 by RVSUM_1:52 ;

hence 1 * v = v ; :: thesis: verum

end;reconsider v1 = v as Element of REAL n by Def6;

reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;

1 * v = (Euclid_mult n) . (1,v1) by Def6

.= 1 * v2 by Def2

.= v2 by RVSUM_1:52 ;

hence 1 * v = v ; :: thesis: verum

thus REAL-US n is Abelian :: thesis: ( REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )

proof

for u, v, w being Element of (REAL-US n) holds (u + v) + w = u + (v + w)
let v, w be VECTOR of (REAL-US n); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v

reconsider v1 = v, w1 = w as Element of REAL n by Def6;

thus v + w = (Euclid_add n) . (v,w) by Def6

.= (Euclid_add n) . (w1,v1) by BINOP_1:def 2

.= w + v by Def6 ; :: thesis: verum

end;reconsider v1 = v, w1 = w as Element of REAL n by Def6;

thus v + w = (Euclid_add n) . (v,w) by Def6

.= (Euclid_add n) . (w1,v1) by BINOP_1:def 2

.= w + v by Def6 ; :: thesis: verum

proof

hence
REAL-US n is add-associative
; :: thesis: ( REAL-US n is right_zeroed & REAL-US n is right_complementable )
let u, v, w be Element of (REAL-US n); :: thesis: (u + v) + w = u + (v + w)

reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def6;

reconsider u2 = u1, v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;

A22: u + (v + w) = (Euclid_add n) . (u1,(v + w)) by Def6

.= (Euclid_add n) . (u2,((Euclid_add n) . (v2,w2))) by Def6

.= (Euclid_add n) . (u2,(v1 + w1)) by Def1 ;

(u + v) + w = (Euclid_add n) . ((u + v),w1) by Def6

.= (Euclid_add n) . (((Euclid_add n) . (u1,v1)),w1) by Def6

.= (Euclid_add n) . ((u1 + v1),w1) by Def1

.= (u1 + v1) + w2 by Def1

.= u2 + (v2 + w2) by RVSUM_1:15 ;

hence (u + v) + w = u + (v + w) by A22, Def1; :: thesis: verum

end;reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def6;

reconsider u2 = u1, v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;

A22: u + (v + w) = (Euclid_add n) . (u1,(v + w)) by Def6

.= (Euclid_add n) . (u2,((Euclid_add n) . (v2,w2))) by Def6

.= (Euclid_add n) . (u2,(v1 + w1)) by Def1 ;

(u + v) + w = (Euclid_add n) . ((u + v),w1) by Def6

.= (Euclid_add n) . (((Euclid_add n) . (u1,v1)),w1) by Def6

.= (Euclid_add n) . ((u1 + v1),w1) by Def1

.= (u1 + v1) + w2 by Def1

.= u2 + (v2 + w2) by RVSUM_1:15 ;

hence (u + v) + w = u + (v + w) by A22, Def1; :: thesis: verum

for v being Element of (REAL-US n) holds v + (0. (REAL-US n)) = v

proof

hence
REAL-US n is right_zeroed
; :: thesis: REAL-US n is right_complementable
let v be Element of (REAL-US n); :: thesis: v + (0. (REAL-US n)) = v

reconsider v1 = v as Element of REAL n by Def6;

v + (0. (REAL-US n)) = (Euclid_add n) . (v,(0. (REAL-US n))) by Def6

.= (Euclid_add n) . (v1,(0* n)) by Def6

.= v1 + (0* n) by Def1 ;

hence v + (0. (REAL-US n)) = v by EUCLID_4:1; :: thesis: verum

end;reconsider v1 = v as Element of REAL n by Def6;

v + (0. (REAL-US n)) = (Euclid_add n) . (v,(0. (REAL-US n))) by Def6

.= (Euclid_add n) . (v1,(0* n)) by Def6

.= v1 + (0* n) by Def1 ;

hence v + (0. (REAL-US n)) = v by EUCLID_4:1; :: thesis: verum

let v be Element of (REAL-US n); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

reconsider v1 = v as Element of REAL n by Def6;

reconsider w = - v1 as Element of (REAL-US n) by Def6;

take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (REAL-US n)

thus v + w = (Euclid_add n) . (v1,(- v1)) by Def6

.= v1 + (- v1) by Def1

.= 0* n by EUCLIDLP:2

.= 0. (REAL-US n) by Def6 ; :: thesis: verum