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