let G be left-distributive doubleLoop; :: thesis: for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a)
let x, y, a 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 Th21 ; :: thesis: verum