let X be RealLinearSpace; :: thesis: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real
set XP = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);
Q1: ( ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-distributive & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is vector-distributive & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-associative & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-unital )

proof

now :: thesis: for x, y being Element of F_Real
for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds (x + y) * v = (x * v) + (y * v)

let x, y be Element of F_Real; :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds (x + y) * v = (x * v) + (y * v)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider v1 = v as Element of X ;
reconsider x1 = x, y1 = y as Real ;
( (x + y) * v = (x1 + y1) * v1 & (x1 + y1) * v1 = (x1 * v1) + (y1 * v1) ) by RLVECT_1:def 6;
hence (x + y) * v = (x * v) + (y * v) ; :: thesis: verum

end;

hence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-distributive ; :: thesis: ( ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is vector-distributive & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-associative & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-unital )

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

let x be Element of F_Real; :: thesis: for v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds x * (v + w) = (x * v) + (x * w)
let v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider v1 = v, w1 = w as Element of X ;
reconsider x1 = x as Real ;
x * (v + w) = x1 * (v1 + w1)
.= (x1 * v1) + (x1 * w1) by RLVECT_1:def 5 ;
hence x * (v + w) = (x * v) + (x * w) ; :: thesis: verum

end;

hence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is vector-distributive ; :: thesis: ( ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-associative & ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-unital )

now :: thesis: for x, y being Element of F_Real
for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds (x * y) * v = x * (y * v)

let x, y be Element of F_Real; :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds (x * y) * v = x * (y * v)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: (x * y) * v = x * (y * v)
reconsider v1 = v as Element of X ;
reconsider x1 = x, y1 = y as Real ;
(x * y) * v = (x1 * y1) * v1
.= x1 * (y1 * v1) by RLVECT_1:def 7 ;
hence (x * y) * v = x * (y * v) ; :: thesis: verum

end;

hence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-associative ; :: thesis: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-unital

now :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) holds (1. F_Real) * v = v

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: (1. F_Real) * v = v
reconsider v1 = v as Element of X ;
(1. F_Real) * v = 1 * v1 ;
hence (1. F_Real) * v = v by RLVECT_1:def 8; :: thesis: verum

end;

hence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is scalar-unital ; :: thesis: verum

end;

now :: thesis: for u, v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* 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,(MultF_Real* X) #); :: thesis: u + (v + w) = (u + v) + w
reconsider u1 = u, v1 = v, w1 = w as Element of X ;
u + (v + w) = u1 + (v1 + w1)
.= (u1 + v1) + w1 by RLVECT_1:def 3 ;
hence u + (v + w) = (u + v) + w ; :: thesis: verum

end;

then Q2: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is add-associative ;

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

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #)) = v
reconsider v1 = v as Element of X ;
v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #)) = v1 + (0. X) ;
hence v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #)) = v ; :: thesis: verum

end;

then Q3: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is right_zeroed ;

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

let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #); :: thesis: v is right_complementable
reconsider v1 = v as Element of X ;
consider w1 being Element of X such that
A1: 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,(MultF_Real* X) #) ;
v + w = 0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) by A1;
hence v is right_complementable ; :: thesis: verum

end;

then Q4: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is right_complementable ;

now :: thesis: for v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* 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,(MultF_Real* X) #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of X ;
v + w = v1 + w1
.= w1 + v1 ;
hence v + w = w + v ; :: thesis: verum

end;

then ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is Abelian ;
hence ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real by Q1, Q2, Q3, Q4; :: thesis: verum