set G = V . W;

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

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;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

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;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

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

let x be Element of (V . W); :: according to ALGSTR_0:def 16 :: thesis: x 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;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

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