set E = S;
set F = R;
set P = VecSp (S,R);
A1: 0. (VecSp (S,R)) = 0. S by Def5;

hereby :: according to RLVECT_1:def 2 :: thesis: ( VecSp (S,R) is add-associative & VecSp (S,R) is right_zeroed & VecSp (S,R) is right_complementable )

let x, y be Element of (VecSp (S,R)); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of S by Def5;
thus x + y = a + b by Def5
.= b + a by RLVECT_1:def 2
.= y + x by Def5 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( VecSp (S,R) is right_zeroed & VecSp (S,R) is right_complementable )

let x, y, z be Element of (VecSp (S,R)); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of S by Def5;
A2: y + z = b + c by Def5;
x + y = a + b by Def5;
hence (x + y) + z = (a + b) + c by Def5
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A2, Def5 ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: VecSp (S,R) is right_complementable

let x be Element of (VecSp (S,R)); :: thesis: x + (0. (VecSp (S,R))) = x
reconsider a = x as Element of S by Def5;
thus x + (0. (VecSp (S,R))) = a + (0. S) by A1, Def5
.= x ; :: thesis: verum

end;

let x be Element of (VecSp (S,R)); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider a = x as Element of S by Def5;
consider b being Element of S such that
A3: a + b = 0. S by ALGSTR_0:def 11;
reconsider y = b as Element of (VecSp (S,R)) by Def5;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (VecSp (S,R))
thus x + y = a + b by Def5
.= 0. (VecSp (S,R)) by A3, Def5 ; :: thesis: verum