set ZS = Gauss_RAT_Module ;
set AG = G_RAT_SET ;
set AD = the addF of Gauss_RAT_Module;
set CA = the carrier of Gauss_RAT_Module;
set Z0 = the ZeroF of Gauss_RAT_Module;
set MLI = RSc_Mult ;
A1: for v, w being Element of Gauss_RAT_Module holds v + w = w + v

proof

let v, w be Element of Gauss_RAT_Module; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as G_RAT by Th10;
thus v + w = v1 + w1 by Th27
.= w + v by Th27 ; :: thesis: verum

end;

A2: for u, v, w being Element of Gauss_RAT_Module holds (u + v) + w = u + (v + w)

proof

let u, v, w be Element of Gauss_RAT_Module; :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as G_RAT by Th10;
A3: u + v = u1 + v1 by Th27;
A4: v + w = v1 + w1 by Th27;
thus (u + v) + w = (u1 + v1) + w1 by Th27, A3
.= u1 + (v1 + w1)
.= u + (v + w) by Th27, A4 ; :: thesis: verum

end;

A5: for v being Element of Gauss_RAT_Module holds v + (0. Gauss_RAT_Module) = v

proof

let v be Element of Gauss_RAT_Module; :: thesis: v + (0. Gauss_RAT_Module) = v
reconsider v1 = v as G_RAT by Th10;
thus v + (0. Gauss_RAT_Module) = v1 + 0 by Th27
.= v ; :: thesis: verum

end;

A6: for v being Element of Gauss_RAT_Module holds v is right_complementable

proof

let v be Element of Gauss_RAT_Module; :: thesis: v is right_complementable
reconsider m1 = - 1 as Element of F_Rat by RAT_1:def 2;
take m1 * v ; :: according to ALGSTR_0:def 11 :: thesis: v + (m1 * v) = 0. Gauss_RAT_Module
reconsider v1 = v as G_RAT by Th10;
A7: m1 * v = (- 1) * v1 by Th28
.= - v1 ;
thus v + (m1 * v) = v1 + (- v1) by A7, Th27
.= 0. Gauss_RAT_Module ; :: thesis: verum

end;

A8: for a, b being Element of F_Rat
for v being Element of Gauss_RAT_Module holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be Element of F_Rat; :: thesis: for v being Element of Gauss_RAT_Module holds (a + b) * v = (a * v) + (b * v)
let v be Element of Gauss_RAT_Module; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as G_RAT by Th10;
reconsider a1 = a, b1 = b as Element of RAT ;
A10: ( a1 * v1 = a * v & b1 * v1 = b * v ) by Th28;
thus (a + b) * v = (a1 + b1) * v1 by Th28
.= (a1 * v1) + (b1 * v1)
.= (a * v) + (b * v) by A10, Th27 ; :: thesis: verum

end;

A11: for a being Element of F_Rat
for v, w being Element of Gauss_RAT_Module holds a * (v + w) = (a * v) + (a * w)

proof

let a be Element of F_Rat; :: thesis: for v, w being Element of Gauss_RAT_Module holds a * (v + w) = (a * v) + (a * w)
let v, w be Element of Gauss_RAT_Module; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as G_RAT by Th10;
reconsider a1 = a as Element of RAT ;
A12: v + w = v1 + w1 by Th27;
A13: ( a1 * v1 = a * v & a1 * w1 = a * w ) by Th28;
thus a * (v + w) = a1 * (v1 + w1) by A12, Th28
.= (a1 * v1) + (a1 * w1)
.= (a * v) + (a * w) by A13, Th27 ; :: thesis: verum

end;

A14: for a, b being Element of F_Rat
for v being Element of Gauss_RAT_Module holds (a * b) * v = a * (b * v)

proof

let a, b be Element of F_Rat; :: thesis: for v being Element of Gauss_RAT_Module holds (a * b) * v = a * (b * v)
let v be Element of Gauss_RAT_Module; :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as G_RAT by Th10;
reconsider a1 = a, b1 = b as Element of RAT ;
A15: b1 * v1 = b * v by Th28;
thus (a * b) * v = (a1 * b1) * v1 by Th28
.= a1 * (b1 * v1)
.= a * (b * v) by A15, Th28 ; :: thesis: verum

end;

for v being Element of Gauss_RAT_Module holds (1. F_Rat) * v = v

proof

let v be Element of Gauss_RAT_Module; :: thesis: (1. F_Rat) * v = v
reconsider i = 1 as Element of F_Rat ;
reconsider v1 = v as G_RAT by Th10;
thus (1. F_Rat) * v = 1 * v1 by Th28
.= v ; :: thesis: verum

end;

hence ( Gauss_RAT_Module is scalar-distributive & Gauss_RAT_Module is vector-distributive & Gauss_RAT_Module is scalar-associative & Gauss_RAT_Module is scalar-unital & Gauss_RAT_Module is add-associative & Gauss_RAT_Module is right_zeroed & Gauss_RAT_Module is right_complementable & Gauss_RAT_Module is Abelian ) by A1, A2, A5, A6, A8, A11, A14, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum