let K be Ring; :: thesis: for r being Scalar of K

for V being LeftMod of K

for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let r be Scalar of K; :: thesis: for V being LeftMod of K

for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let V be LeftMod of K; :: thesis: for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let a, b be Vector of V; :: thesis: for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let W be Subspace of V; :: thesis: ( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

thus (a / W) + (b / W) = (a . W) + (b . W)

.= (a + b) / W by Th17 ; :: thesis: r * (a / W) = (r * a) / W

thus r * (a / W) = (LMULT W) . (r,(a . W)) by VECTSP_1:def 12

.= r * (a . W) by Def21

.= (r * a) / W by Def20 ; :: thesis: verum

for V being LeftMod of K

for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let r be Scalar of K; :: thesis: for V being LeftMod of K

for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let V be LeftMod of K; :: thesis: for a, b being Vector of V

for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let a, b be Vector of V; :: thesis: for W being Subspace of V holds

( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

let W be Subspace of V; :: thesis: ( (a / W) + (b / W) = (a + b) / W & r * (a / W) = (r * a) / W )

thus (a / W) + (b / W) = (a . W) + (b . W)

.= (a + b) / W by Th17 ; :: thesis: r * (a / W) = (r * a) / W

thus r * (a / W) = (LMULT W) . (r,(a . W)) by VECTSP_1:def 12

.= r * (a . W) by Def21

.= (r * a) / W by Def20 ; :: thesis: verum