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

proof

thus VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is Abelian :: thesis: ( VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is add-associative & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_zeroed & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable )

proof

let a, b be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: 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: ( VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_zeroed & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable )

let a, b, c be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: 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: VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable

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

end;

let a be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: 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 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) ;
take b9 ; :: according to ALGSTR_0:def 11 :: thesis: a + b9 = 0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #)
thus a + b9 = 0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) by A3; :: thesis: verum

end;

now

let x, y be Scalar of R; :: thesis: for v, w being Vector of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) 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 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: 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 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) 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