let V be non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let V1 be non empty Subset of V; :: thesis: for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let d1 be Element of V1; :: thesis: for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let A be BinOp of V1; :: thesis: for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
let M be Function of [:REAL,V1:],V1; :: thesis: ( d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] implies ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital ) )
set D = V1;
assume that
A1: d1 = 0. V and
A2: A = the addF of V || V1 and
A3: M = the Mult of V | [:REAL,V1:] ; :: thesis: ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
set W = RLSStruct(# V1,d1,A,M #);

A4: now

let a be Real; :: thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds a * x = the Mult of V . (a,x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: a * x = the Mult of V . (a,x)
thus a * x = the Mult of V . [a,x] by A3, FUNCT_1:49
.= the Mult of V . (a,x) ; :: thesis: verum

end;

A5: now

let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: x + y = the addF of V . (x,y)
thus x + y = the addF of V . [x,y] by A2, FUNCT_1:49
.= the addF of V . (x,y) ; :: thesis: verum

end;

( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

proof

set Mv = the Mult of V;
set Av = the addF of V;

hereby :: according to RLVECT_1:def 2 :: thesis: ( RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
thus x + y = x1 + y1 by A5
.= y1 + x1
.= y + x by A5 ; :: thesis: verum

end;

now

let x, y, z be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by TARSKI:def 3;
thus (x + y) + z = the addF of V . ((x + y),z1) by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= the addF of V . (x1,(y + z)) by A5
.= x + (y + z) by A5 ; :: thesis: verum

end;

hence RLSStruct(# V1,d1,A,M #) is add-associative by RLVECT_1:def 3; :: thesis: ( RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

now

let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: x + (0. RLSStruct(# V1,d1,A,M #)) = x
reconsider y = x as VECTOR of V by TARSKI:def 3;
thus x + (0. RLSStruct(# V1,d1,A,M #)) = y + (0. V) by A1, A5
.= x by RLVECT_1:def 4 ; :: thesis: verum

end;

hence RLSStruct(# V1,d1,A,M #) is right_zeroed by RLVECT_1:def 4; :: thesis: ( RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

hereby :: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

let a1 be real number ; :: thesis: for x, y being VECTOR of RLSStruct(# V1,d1,A,M #) holds a1 * (x + y) = (a1 * x) + (a1 * y)
let x, y be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: a1 * (x + y) = (a1 * x) + (a1 * y)
reconsider a = a1 as Real by XREAL_0:def 1;
reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
a * (x + y) = the Mult of V . (a,(x + y)) by A4
.= a * (x1 + y1) by A5
.= (a * x1) + (a * y1) by RLVECT_1:def 5
.= the addF of V . (( the Mult of V . (a,x1)),(a * y)) by A4
.= the addF of V . ((a * x),(a * y)) by A4
.= (a * x) + (a * y) by A5 ;
hence a1 * (x + y) = (a1 * x) + (a1 * y) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

let a1, b1 be real number ; :: thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds (a1 + b1) * x = (a1 * x) + (b1 * x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: (a1 + b1) * x = (a1 * x) + (b1 * x)
reconsider a = a1, b = b1 as Real by XREAL_0:def 1;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a + b) * x = (a + b) * y by A4
.= (a * y) + (b * y) by RLVECT_1:def 6
.= the addF of V . (( the Mult of V . (a,y)),(b * x)) by A4
.= the addF of V . ((a * x),(b * x)) by A4
.= (a * x) + (b * x) by A5 ;
hence (a1 + b1) * x = (a1 * x) + (b1 * x) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: RLSStruct(# V1,d1,A,M #) is scalar-unital

let a1, b1 be real number ; :: thesis: for x being VECTOR of RLSStruct(# V1,d1,A,M #) holds (a1 * b1) * x = a1 * (b1 * x)
let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: thesis: (a1 * b1) * x = a1 * (b1 * x)
reconsider a = a1, b = b1 as Real by XREAL_0:def 1;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a * b) * x = (a * b) * y by A4
.= a * (b * y) by RLVECT_1:def 7
.= the Mult of V . (a,(b * x)) by A4
.= a * (b * x) by A4 ;
hence (a1 * b1) * x = a1 * (b1 * x) ; :: thesis: verum

end;

let x be VECTOR of RLSStruct(# V1,d1,A,M #); :: according to RLVECT_1:def 8 :: thesis: 1 * x = x
reconsider y = x as VECTOR of V by TARSKI:def 3;
thus 1 * x = 1 * y by A4
.= x by RLVECT_1:def 8 ; :: thesis: verum

end;

hence ( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital ) ; :: thesis: verum