let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)
let x, y, z be Element of F; :: thesis: x * (y - z) = (x * y) - (x * z)
x * (y - z) = (x * y) + (x * (- z)) by Def2
.= (x * y) - (x * z) by Th4 ;
hence x * (y - z) = (x * y) - (x * z) ; :: thesis: verum