let F be Field; for a, b, c, d, e, h being Element of F st a <> 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; ( a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume that
A1:
a <> 0. F
and
A2:
(a * e) - (d * b) = 0. F
and
A3:
(a * c) - (h * b) = 0. F
; (d * c) - (h * e) = 0. F
c = (h * b) * (a ")
by A1, A3, VECTSP_1:30;
then
c = h * (b * (a "))
by GROUP_1:def 3;
then A4:
d * c = (d * h) * (b * (a "))
by GROUP_1:def 3;
e = (d * b) * (a ")
by A1, A2, VECTSP_1:30;
then
e = d * (b * (a "))
by GROUP_1:def 3;
then
h * e = (h * d) * (b * (a "))
by GROUP_1:def 3;
hence
(d * c) - (h * e) = 0. F
by A4, RLVECT_1:15; verum