let F be Field; :: thesis: for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F
let a, b, c, d be Element of F; :: thesis: (a * (b - b)) - ((c - c) * d) = 0. F
c - c = 0. F by RLVECT_1:15;
then A1: (c - c) * d = 0. F ;
b - b = 0. F by RLVECT_1:15;
then a * (b - b) = 0. F ;
hence (a * (b - b)) - ((c - c) * d) = 0. F by A1, RLVECT_1:15; :: thesis: verum