set X0 = the carrier of X;
set Z0 = the ZeroF of X;
set ADD = the addF of X;
set LMLT = Mult_INT* X;
set XP = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);
A1: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is vector-distributive

proof

let x be Scalar of R; :: according to VECTSP_1:def 13 :: thesis: for b₁, b₂ being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds x * (b₁ + b₂) = (x * b₁) + (x * b₂)
let v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: x * (v + w) = (x * v) + (x * w)
set x1 = x;
reconsider v1 = v, w1 = w as Element of X ;
thus x * (v + w) = x * (v1 + w1)
.= (x * v1) + (x * w1) by VECTSP_1:def 14
.= (x * v) + (x * w) ; :: thesis: verum

end;

A2: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-distributive

proof

let x, y be Scalar of R; :: according to VECTSP_1:def 14 :: thesis: for b₁ being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds (x + y) * b₁ = (x * b₁) + (y * b₁)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: (x + y) * v = (x * v) + (y * v)
set x1 = x;
set y1 = y;
reconsider v1 = v as Element of X ;
thus (x + y) * v = (x + y) * v1
.= (x * v1) + (y * v1) by VECTSP_1:def 15
.= (x * v) + (y * v) ; :: thesis: verum

end;

A3: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-associative

proof

let x, y be Scalar of R; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds (x * y) * b₁ = x * (y * b₁)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: (x * y) * v = x * (y * v)
set x1 = x;
set y1 = y;
reconsider v1 = v as Element of X ;
thus (x * y) * v = (x * y) * v1
.= x * (y * v1) by VECTSP_1:def 16
.= x * (y * v) ; :: thesis: verum

end;

A4: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-unital

proof

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: according to VECTSP_1:def 16 :: thesis: (1. R) * v = v
reconsider v1 = v as Element of X ;
thus (1. R) * v = (1. R) * v1
.= v1
.= v ; :: thesis: verum

end;

A5: now :: thesis: for u, v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds u + (v + w) = (u + v) + w

let u, v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: u + (v + w) = (u + v) + w
reconsider u1 = u, v1 = v, w1 = w as Element of X ;
thus u + (v + w) = u1 + (v1 + w1)
.= (u1 + v1) + w1 by RLVECT_1:def 3
.= (u + v) + w ; :: thesis: verum

end;

A6: now :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #)) = v

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #)) = v
reconsider v1 = v as Element of X ;
thus v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #)) = v1 + (0. X)
.= v by RLVECT_1:def 4 ; :: thesis: verum

end;

A7: now :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds v is right_complementable

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: v is right_complementable
reconsider v1 = v as Element of X ;
consider w1 being Element of X such that
A8: v1 + w1 = 0. X by ALGSTR_0:def 11;
reconsider w = w1 as Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) ;
v + w = 0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) by A8;
hence v is right_complementable ; :: thesis: verum

end;

now :: thesis: for v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) holds v + w = w + v

let v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of X ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum

end;

hence ( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is vector-distributive & modetrans X is scalar-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital ) by A1, A2, A3, A4, A5, A6, A7; :: thesis: verum