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

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

A2:
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-distributive
let x be Scalar of R; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} 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_{1} + b_{2}) = (x * b_{1}) + (x * b_{2})

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;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

proof

A3:
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-associative
let x, y be Scalar of R; :: according to VECTSP_1:def 14 :: thesis: for b_{1} 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_{1} = (x * b_{1}) + (y * b_{1})

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;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

proof

A4:
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #) is scalar-unital
let x, y be Scalar of R; :: according to VECTSP_1:def 15 :: thesis: for b_{1} 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_{1} = x * (y * b_{1})

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;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

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 by VECTSP_1:def 17

.= v ; :: thesis: verum

end;reconsider v1 = v as Element of X ;

thus (1. R) * v = (1. R) * v1

.= v1 by VECTSP_1:def 17

.= v ; :: thesis: verum

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;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

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;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

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;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

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

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: verumlet 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;reconsider v1 = v, w1 = w as Element of X ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum