let K be Ring; :: 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 & 0. (V . W) = (0. V) . 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 & 0. (V . W) = (0. V) . W )
let a, b be Vector of V; :: thesis: for W being Subspace of V holds
( (a . W) + (b . W) = (a + b) . W & 0. (V . W) = (0. V) . W )
let W be Subspace of V; :: thesis: ( (a . W) + (b . W) = (a + b) . W & 0. (V . W) = (0. V) . W )
thus (a . W) + (b . W) = (a .. W) + (b .. W) by Def17
.= (a + b) . W by Def15 ; :: thesis: 0. (V . W) = (0. V) . W
thus 0. (V . W) = (0. V) . W ; :: thesis: verum