let F be Field; :: thesis: for a, b, c, d, e, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
let a, b, c, d, e, h be Element of F; :: thesis: ( b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume b <> 0. F ; :: thesis: ( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F )
then ( (b * d) - (e * a) = 0. F & (b * h) - (c * a) = 0. F implies (e * h) - (c * d) = 0. F ) by Lm4;
hence ( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F ) by Lm5; :: thesis: verum