let AG be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module
reconsider ZS = ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) as non empty ModuleStr over INT.Ring ;
set ML = the lmult of ZS;
set AD = the addF of ZS;
set CA = the carrier of ZS;
set Z0 = the ZeroF of ZS;
set MLI = Int-mult-left AG;
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 AG ;
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 AG ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

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

proof

let v be Vector of ZS; :: thesis: v + (0. ZS) = v
reconsider v1 = v as Element of AG ;
thus v + (0. ZS) = v1 + (0. AG)
.= v by RLVECT_1:def 4 ; :: thesis: verum

end;

A4: now :: thesis: for v being Vector of ZS holds v is right_complementable

let v be Vector of ZS; :: thesis: v is right_complementable
reconsider v1 = v as Element of AG ;
consider w1 being Element of AG such that
A5: v1 + w1 = 0. AG by ALGSTR_0:def 11;
reconsider w = w1 as Element of ZS ;
v + w = 0. ZS by A5;
hence v is right_complementable ; :: thesis: verum

end;

A6: 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 ;
reconsider v1 = v as Element of AG ;
thus (a + b) * v = ((Int-mult-left AG) . (a,v1)) + ((Int-mult-left AG) . (b,v1)) by Th159
.= (a * v) + (b * v) ; :: thesis: verum

end;

A7: 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 AG ;
thus a * (v + w) = (Int-mult-left AG) . (a1,(v1 + w1))
.= ((Int-mult-left AG) . (a1,v1)) + ((Int-mult-left AG) . (a1,w1)) by Th161
.= (a * v) + (a * w) ; :: thesis: verum

end;

A8: for a, b being Element of INT.Ring
for v being Vector of ZS holds (a * b) * v = a * (b * v) by Th163;
for v being Vector of ZS holds (1. INT.Ring) * v = v by Th155;
hence ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module by A1, A2, A3, A4, A6, A7, A8, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum