let V be Z_Module; for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real; ( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
set L = GenLat (V,sc);
A1:
for x, y being Vector of (GenLat (V,sc))
for x9, y9 being Vector of V st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for a being Element of INT.Ring holds a * x = a * x9 ) )
;
thus
for v, w being Vector of (GenLat (V,sc)) holds v + w = w + v
RLVECT_1:def 2 ( GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
for u, v, w being Vector of (GenLat (V,sc)) holds (u + v) + w = u + (v + w)
RLVECT_1:def 3 ( GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
for v being Vector of (GenLat (V,sc)) holds v + (0. (GenLat (V,sc))) = v
RLVECT_1:def 4 ( GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
GenLat (V,sc) is right_complementable
( GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
for a, b being Element of INT.Ring
for v being Vector of (GenLat (V,sc)) holds (a + b) * v = (a * v) + (b * v)
VECTSP_1:def 14 ( GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
for a being Element of INT.Ring
for v, w being Vector of (GenLat (V,sc)) holds a * (v + w) = (a * v) + (a * w)
VECTSP_1:def 13 ( GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
thus
for a, b being Element of INT.Ring
for v being Vector of (GenLat (V,sc)) holds (a * b) * v = a * (b * v)
VECTSP_1:def 15 GenLat (V,sc) is scalar-unital
thus
for v being Vector of (GenLat (V,sc)) holds (1. INT.Ring) * v = v
VECTSP_1:def 16 verum