let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)
let y, z, x be Element of K; :: thesis: (y - z) * x = (y * x) - (z * x)
thus (y - z) * x = (y * x) + ((- z) * x) by Def3
.= (y * x) - (z * x) by Th5 ; :: thesis: verum