set G = V . W;

hereby :: according to RLVECT_1:def 5 :: 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 Th22;
consider b being Vector of V such that
A2: y = b . W by Th22;
( x + y = (a + b) . W & y + x = (b + a) . W ) by A1, A2, Th24;
hence x + y = y + x ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: 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 Th22;
consider b being Vector of V such that
A4: y = b . W by Th22;
consider c being Vector of V such that
A5: z = c . W by Th22;
A6: ( x + y = (a + b) . W & y + x = (b + a) . W & y + z = (b + c) . W ) by A3, A4, A5, Th24;
hence (x + y) + z = ((a + b) + c) . W by A5, Th24
.= (a + (b + c)) . W by RLVECT_1:def 6
.= x + (y + z) by A3, A6, Th24 ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: 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
A7: x = a . W by Th22;
0. (V . W) = (0. V) . W ;
hence x + (0. (V . W)) = (a + (0. V)) . W by A7, Th24
.= x by A7, RLVECT_1:10 ;
:: 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
A8: x = a . W by Th22;
consider b being Vector of V such that
A9: a + b = 0. V by ALGSTR_0:def 11;
reconsider b' = b . W as Element of (V . W) ;
take b' ; :: according to ALGSTR_0:def 11 :: thesis: x + b' = 0. (V . W)
thus x + b' = (0. V) . W by A8, A9, Th24
.= 0. (V . W) ; :: thesis: verum