let X be VectSp of F_Real ; :: thesis: RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is RealLinearSpace
set XQ = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);
A1: for vZ1, wZ1 being Element of X
for v, w being Element of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) st v = vZ1 & w = wZ1 holds
v + w = vZ1 + wZ1 ;
( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is Abelian & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is add-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_zeroed & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_complementable & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

proof

hereby :: according to RLVECT_1:def 2 :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is add-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_zeroed & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_complementable & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

let v, w be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: v + w = w + v
reconsider vZ1 = v, wZ1 = w as Element of X ;
thus v + w = wZ1 + vZ1 by A1
.= w + v ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_zeroed & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_complementable & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

let u, v, w be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: (u + v) + w = u + (v + w)
reconsider uZ1 = u, vZ1 = v, wZ1 = w as Element of X ;
(u + v) + w = (uZ1 + vZ1) + wZ1
.= uZ1 + (vZ1 + wZ1) by RLVECT_1:def 3 ;
hence (u + v) + w = u + (v + w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_complementable & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

let v be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: v + (0. RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #)) = v
reconsider vZ1 = v as Element of X ;
thus v + (0. RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #)) = vZ1 + (0. X)
.= v ; :: thesis: verum

end;

thus RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is right_complementable :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

proof

let v be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider vZ1 = v as Element of X ;
consider wZ1 being Element of X such that
A2: vZ1 + wZ1 = 0. X by ALGSTR_0:def 11;
reconsider w = wZ1 as VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #)
thus v + w = 0. RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) by A2; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is vector-distributive & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

let a, b be Real; :: thesis: for v being VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider vZ1 = v as Element of X ;
reconsider aZ1 = a, bZ1 = b as Element of F_Real by XREAL_0:def 1;
(a + b) * v = (aZ1 + bZ1) * vZ1
.= (aZ1 * vZ1) + (bZ1 * vZ1) by VECTSP_1:def 15 ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-associative & RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital )

let a be Real; :: thesis: for v, w being VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider aZ1 = a as Element of F_Real by XREAL_0:def 1;
reconsider vZ1 = v, wZ1 = w as Element of X ;
a * (v + w) = aZ1 * (vZ1 + wZ1)
.= (aZ1 * vZ1) + (aZ1 * wZ1) by VECTSP_1:def 14 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is scalar-unital

let a, b be Real; :: thesis: for v being VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) holds (a * b) * v = a * (b * v)
let v be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: thesis: (a * b) * v = a * (b * v)
reconsider vZ1 = v as Element of X ;
reconsider aZ1 = a, bZ1 = b as Element of F_Real by XREAL_0:def 1;
(a * b) * v = (aZ1 * bZ1) * vZ1
.= aZ1 * (bZ1 * vZ1) by VECTSP_1:def 16 ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
reconsider vZ1 = v as Element of X ;
thus 1 * v = (1. F_Real) * vZ1
.= v ; :: thesis: verum

end;

hence RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #) is RealLinearSpace ; :: thesis: verum