let F be Field; :: thesis: for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds
(d * c) - (b * a) = 0. F
let a, b, c, d be Element of F; :: thesis: ( (a * b) - (c * d) = 0. F implies (d * c) - (b * a) = 0. F )
assume (a * b) - (c * d) = 0. F ; :: thesis: (d * c) - (b * a) = 0. F
then A1: - ((a * b) - (c * d)) = 0. F by RLVECT_1:12;
thus (d * c) - (b * a) = (d * c) + (- (b * a)) by RLVECT_1:def 11
.= 0. F by A1, RLVECT_1:33 ; :: thesis: verum