let R be Ring; :: thesis: VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is strict LeftMod of R
set G = VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #);
set a = 0. Trivial-addLoopStr ;
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 5 :: 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 6 :: 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 6
.= a + (b + c) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: 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:10 ; :: 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 b' = b as Element of VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) ;
take b' ; :: according to ALGSTR_0:def 11 :: thesis: a + b' = 0. VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #)
thus a + b' = 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 )
( x * (v + w) = 0. Trivial-addLoopStr & (x * v) + (x * w) = 0. Trivial-addLoopStr & (x + y) * v = 0. Trivial-addLoopStr & (x * v) + (y * v) = 0. Trivial-addLoopStr & (x * y) * v = 0. Trivial-addLoopStr & x * (y * v) = 0. Trivial-addLoopStr & (1. R) * v = 0. Trivial-addLoopStr & v = 0. Trivial-addLoopStr ) by GRCAT_1:8;
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 ) ; :: thesis: verum

end;

hence VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is strict LeftMod of R by A2, VECTSP_1:def 26; :: thesis: verum