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

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