Lm1: now

take ZS = {0}; :: thesis:
reconsider O = 0 as Element of ZS by TARSKI:def 1;
take O = O; :: thesis:
deffunc H₁( Element of ZS, Element of ZS) -> Element of ZS = O;
consider F being BinOp of ZS such that
A1: for x, y being Element of ZS holds F . x,y = H₁(x,y) from BINOP_1:sch 2( R );
deffunc H₂( Element of REAL , Element of ZS) -> Element of ZS = O;
consider G being Function of [:REAL ,ZS:],ZS such that
A2: for a being Element of REAL
for x being Element of ZS holds G . [a,x] = H₂(a,x) from FUNCT_2:sch 8( REAL R R );
take F = F; :: thesis:
take G = G; :: thesis:
set W = RLSStruct(# ZS,O,F,G #);
thus for x, y being VECTOR of RLSStruct(# ZS,O,F,G #) holds x + y = y + x :: thesis:

proof

let x, y be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
A3: ( x + y = F . x,y & y + x = F . y,x ) ;
reconsider X = x, Y = y as Element of ZS ;
( x + y = H₁(X,Y) & y + x = H₁(Y,X) ) by A1, A3;
hence x + y = y + x ; :: thesis:

end;

thus for x, y, z being VECTOR of RLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) :: thesis:

proof

let x, y, z be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
A4: ( (x + y) + z = F . (x + y),z & x + (y + z) = F . x,(y + z) ) ;
reconsider X = x, Y = y, Z = z as Element of ZS ;
( (x + y) + z = H₁(H₁(X,Y),Z) & x + (y + z) = H₁(X,H₁(Y,Z)) ) by A1, A4;
hence (x + y) + z = x + (y + z) ; :: thesis:

end;

thus for x being VECTOR of RLSStruct(# ZS,O,F,G #) holds x + (0. RLSStruct(# ZS,O,F,G #)) = x :: thesis:

proof

let x be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
x + (0. RLSStruct(# ZS,O,F,G #)) = F . [x,(0. RLSStruct(# ZS,O,F,G #))]
.= F . x,(0. RLSStruct(# ZS,O,F,G #))
.= H₁(X,O) by A1 ;
hence x + (0. RLSStruct(# ZS,O,F,G #)) = x by TARSKI:def 1; :: thesis:

end;

thus for x being VECTOR of RLSStruct(# ZS,O,F,G #) ex y being VECTOR of RLSStruct(# ZS,O,F,G #) st x + y = 0. RLSStruct(# ZS,O,F,G #) :: thesis:

proof

let x be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
reconsider y = O as VECTOR of RLSStruct(# ZS,O,F,G #) ;
take y ; :: thesis:
thus x + y = F . [x,y]
.= F . x,y
.= the Zero of RLSStruct(# ZS,O,F,G #) by A1
.= 0. RLSStruct(# ZS,O,F,G #) ; :: thesis:

end;

thus for a being Real
for x, y being VECTOR of RLSStruct(# ZS,O,F,G #) holds a * (x + y) = (a * x) + (a * y) :: thesis:

proof

let a be Real; :: thesis:
let x, y be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x, Y = y as Element of ZS ;
(a * x) + (a * y) = F . [(a * x),(a * y)]
.= F . (a * x),(a * y)
.= H₁(H₂(a,X),H₂(a,Y)) by A1 ;
hence a * (x + y) = (a * x) + (a * y) by A2; :: thesis:

end;

thus for a, b being Real
for x being VECTOR of RLSStruct(# ZS,O,F,G #) holds (a + b) * x = (a * x) + (b * x) :: thesis:

proof

let a, b be Real;
let x be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
set c = a + b;
reconsider X = x as Element of ZS ;
A5: (a + b) * x = G . [(a + b),x]
.= H₂(a + b,X) by A2 ;
(a * x) + (b * x) = F . [(a * x),(b * x)]
.= F . (a * x),(b * x)
.= H₁(H₂(a,X),H₂(b,X)) by A1 ;
hence (a + b) * x = (a * x) + (b * x) by A5; :: thesis:

end;

thus for a, b being Real
for x being VECTOR of RLSStruct(# ZS,O,F,G #) holds (a * b) * x = a * (b * x) :: thesis:

proof

let a, b be Real;
let x be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
set c = a * b;
reconsider X = x as Element of ZS ;
A6: (a * b) * x = G . [(a * b),x]
.= H₂(a * b,X) by A2 ;
a * (b * x) = G . [a,(b * x)]
.= H₂(a,H₂(b,X)) by A2 ;
hence (a * b) * x = a * (b * x) by A6; :: thesis:

end;

thus for x being VECTOR of RLSStruct(# ZS,O,F,G #) holds 1 * x = x :: thesis:

proof

let x be VECTOR of RLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
reconsider A' = 1 as Element of REAL ;
1 * x = G . [1,x]
.= H₂(A',X) by A2 ;
hence 1 * x = x by TARSKI:def 1; :: thesis:

end;