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

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