let G be Abelian right-distributive doubleLoop; :: thesis: for a, x, y being Element of G holds a * (x - y) = (a * x) - (a * y)
let a, x, y be Element of G; :: thesis: a * (x - y) = (a * x) - (a * y)
thus a * (x - y) = (a * x) + (a * (- y)) by VECTSP_1:def 2
.= (a * x) - (a * y) by Th2 ; :: thesis: verum