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