set ZS = Rat-Module ;
reconsider ZS = Rat-Module as non empty ModuleStr over INT.Ring ;
set AG = the carrier of F_Rat;
set MLI = Int-mult-left F_Rat;
A1: for v, w being Element of ZS holds v + w = w + v

proof

let v, w be Element of ZS; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of F_Rat ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum

end;

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

proof

let u, v, w be Element of ZS; :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of F_Rat ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

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

proof

let v be Element of ZS; :: thesis: v + (0. ZS) = v
reconsider v1 = v as Element of F_Rat ;
thus v + (0. ZS) = v1 + (0. F_Rat)
.= v ; :: thesis: verum

end;

A6: for v being Vector of ZS holds v is right_complementable

proof

let v be Vector of ZS; :: thesis: v is right_complementable
take (- (1. INT.Ring)) * v ; :: according to ALGSTR_0:def 11 :: thesis: v + ((- (1. INT.Ring)) * v) = 0. ZS
reconsider v1 = v as Element of F_Rat ;
set i0 = 0. INT.Ring;
set i1 = 1. INT.Ring;
set i2 = - (1. INT.Ring);
0. F_Rat = (Int-mult-left F_Rat) . (((1. INT.Ring) + (- (1. INT.Ring))),v1) by ZMODUL01:152
.= ((Int-mult-left F_Rat) . ((1. INT.Ring),v1)) + ((Int-mult-left F_Rat) . ((- (1. INT.Ring)),v1)) by ZMODUL01:159
.= v + ((- (1. INT.Ring)) * v) by ZMODUL01:155 ;
hence v + ((- (1. INT.Ring)) * v) = 0. ZS ; :: thesis: verum

end;

A8: for a, b being Element of INT.Ring
for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be Element of INT.Ring; :: thesis: for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)
let v be Vector of ZS; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider a1 = a, b1 = b as Element of INT.Ring ;
reconsider v1 = v as Element of F_Rat ;
thus (a + b) * v = ((Int-mult-left F_Rat) . (a1,v1)) + ((Int-mult-left F_Rat) . (b1,v1)) by ZMODUL01:159
.= (a * v) + (b * v) ; :: thesis: verum

end;

for a being Element of INT.Ring
for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)

proof

let a be Element of INT.Ring; :: thesis: for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)
let v, w be Vector of ZS; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider a1 = a as Element of INT.Ring ;
reconsider v1 = v, w1 = w as Element of F_Rat ;
thus a * (v + w) = (Int-mult-left F_Rat) . (a,(v1 + w1))
.= ((Int-mult-left F_Rat) . (a1,v1)) + ((Int-mult-left F_Rat) . (a1,w1)) by ZMODUL01:161
.= (a * v) + (a * w) ; :: thesis: verum

end;

hence ( Rat-Module is Abelian & Rat-Module is add-associative & Rat-Module is right_zeroed & Rat-Module is right_complementable & Rat-Module is scalar-distributive & Rat-Module is vector-distributive & Rat-Module is scalar-associative & Rat-Module is scalar-unital ) by A1, A2, A5, A6, A8, ZMODUL01:163, ZMODUL01:155, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum