let z1, z2, z3, z4 be Element of F_Complex; ( z2 <> 0. F_Complex & z4 <> 0. F_Complex implies (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4) )
reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;
assume A2:
z2 <> 0. F_Complex
; ( not z4 <> 0. F_Complex or (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4) )
then A3:
z19 / z29 = z1 / z2
by Th6;
assume A4:
z4 <> 0. F_Complex
; (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4)
then A5:
z2 * z4 <> 0. F_Complex
by A2, VECTSP_1:12;
thus (z1 / z2) - (z3 / z4) =
(z19 / z29) - (z39 / z49)
by A3, A4, Th6
.=
((z19 * z49) - (z39 * z29)) / (z29 * z49)
by A2, A4, Th7, XCMPLX_1:130
.=
((z1 * z4) - (z3 * z2)) / (z2 * z4)
by A5, Th6
; verum