let G be left-distributive doubleLoop; :: thesis: for a, x, y being Element of G holds (x - y) * a = (x * a) - (y * a)

let a, x, y be Element of G; :: thesis: (x - y) * a = (x * a) - (y * a)

thus (x - y) * a = (x * a) + ((- y) * a) by VECTSP_1:def 3

.= (x * a) - (y * a) by Th7 ; :: thesis: verum

let a, x, y be Element of G; :: thesis: (x - y) * a = (x * a) - (y * a)

thus (x - y) * a = (x * a) + ((- y) * a) by VECTSP_1:def 3

.= (x * a) - (y * a) by Th7 ; :: thesis: verum