set G = V . W;

hereby :: according to RLVECT_1:def 2 :: thesis: ( V . W is add-associative & V . W is right_zeroed & V . W is right_complementable )

let x, y be Element of (V . W); :: thesis: x + y = y + x
consider a being Vector of V such that
A1: x = a . W by Th15;
consider b being Vector of V such that
A2: y = b . W by Th15;
x + y = (a + b) . W by A1, A2, Th17;
hence x + y = y + x by A1, A2, Th17; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( V . W is right_zeroed & V . W is right_complementable )

let x, y, z be Element of (V . W); :: thesis: (x + y) + z = x + (y + z)
consider a being Vector of V such that
A3: x = a . W by Th15;
consider b being Vector of V such that
A4: y = b . W by Th15;
consider c being Vector of V such that
A5: z = c . W by Th15;
A6: x + y = (a + b) . W by A3, A4, Th17;
A7: y + z = (b + c) . W by A4, A5, Th17;
thus (x + y) + z = ((a + b) + c) . W by A5, A6, Th17
.= (a + (b + c)) . W by RLVECT_1:def 3
.= x + (y + z) by A3, A7, Th17 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: V . W is right_complementable

let x be Element of (V . W); :: thesis: x + (0. (V . W)) = x
consider a being Vector of V such that
A8: x = a . W by Th15;
0. (V . W) = (0. V) . W ;
hence x + (0. (V . W)) = (a + (0. V)) . W by A8, Th17
.= x by A8, RLVECT_1:4 ;
:: thesis: verum

end;

let x be Element of (V . W); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
consider a being Vector of V such that
A9: x = a . W by Th15;
consider b being Vector of V such that
A10: a + b = 0. V by ALGSTR_0:def 11;
reconsider b9 = b . W as Element of (V . W) ;
take b9 ; :: according to ALGSTR_0:def 11 :: thesis: x + b9 = 0. (V . W)
thus x + b9 = (0. V) . W by A9, A10, Th17
.= 0. (V . W) ; :: thesis: verum