let x, y, z be Element of (opp K); :: according to VECTSP_1:def 7 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider a = x, b = y, c = z as Element of K ;
thus x * (y + z) = (b + c) * a by Lm4
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (x * y) + (x * z) by Lm4 ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = a * (b + c) by Lm4
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (y * x) + (z * x) by Lm4 ; :: thesis: verum