let R be Ring; :: thesis: ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is strict LeftMod of R
set a = 0. Trivial-addLoopStr;
set G = ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #);
A1: for a, b being Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #)
for x, y being Element of Trivial-addLoopStr st x = a & b = y holds
a + b = x + y ;
A2: ( ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is Abelian & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is add-associative & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_zeroed & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_complementable )

proof

thus ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is Abelian :: thesis: ( ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is add-associative & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_zeroed & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_complementable )

proof

let a, b be Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of Trivial-addLoopStr ;
thus a + b = y + x by A1
.= b + a ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_zeroed & ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_complementable )

let a, b, c be Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of Trivial-addLoopStr ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is right_complementable

let a be Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #); :: thesis: a + (0. ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #)) = a
reconsider x = a as Element of Trivial-addLoopStr ;
thus a + (0. ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #)) = x + (0. Trivial-addLoopStr)
.= a by RLVECT_1:4 ; :: thesis: verum

end;

let a be Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of Trivial-addLoopStr ;
consider b being Element of Trivial-addLoopStr such that
A3: x + b = 0. Trivial-addLoopStr by ALGSTR_0:def 11;
reconsider b9 = b as Element of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) ;
take b9 ; :: according to ALGSTR_0:def 11 :: thesis: a + b9 = 0. ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #)
thus a + b9 = 0. ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) by A3; :: thesis: verum

end;

now :: thesis: for x, y being Scalar of R
for v, w being Vector of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )

let x, y be Scalar of R; :: thesis: for v, w being Vector of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
let v, w be Vector of ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
A4: ( (x * y) * v = 0. Trivial-addLoopStr & (1. R) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
( x * (v + w) = 0. Trivial-addLoopStr & (x + y) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
hence ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v ) by A4, GRCAT_1:4; :: thesis: verum

end;

hence ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #) is strict LeftMod of R by A2, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; :: thesis: verum