let F be Field; :: thesis: for a, b, c, d, f, g being Element of F st (a * b) - (c * d) = 0. F holds
(((a * f) * g) * b) - (((c * f) * g) * d) = 0. F
let a, b, c, d, f, g be Element of F; :: thesis: ( (a * b) - (c * d) = 0. F implies (((a * f) * g) * b) - (((c * f) * g) * d) = 0. F )
assume A1: (a * b) - (c * d) = 0. F ; :: thesis: (((a * f) * g) * b) - (((c * f) * g) * d) = 0. F
( ((a * f) * g) * b = (f * g) * (a * b) & ((c * f) * g) * d = (f * g) * (c * d) ) by Lm7;
hence (((a * f) * g) * b) - (((c * f) * g) * d) = (f * g) * ((a * b) - (c * d)) by VECTSP_1:11
.= 0. F by A1 ;
:: thesis: verum