let z, z1, z2 be Element of F_Complex; :: thesis: ( z <> 0. F_Complex & z2 <> 0. F_Complex implies ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) ) )
reconsider z19 = z1, z29 = z2, z9 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; :: thesis: ( not z2 <> 0. F_Complex or ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) ) )
assume A2: z2 <> 0. F_Complex ; :: thesis: ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) )
then A3: z2 * z <> 0. F_Complex by A1, VECTSP_1:12;
thus z1 / z2 = z19 / z29 by A2, Th6
.= (z19 * z9) / (z29 * z9) by A1, Th7, XCMPLX_1:91
.= (z1 * z) / (z2 * z) by A3, Th6 ; :: thesis: z1 / z2 = (z * z1) / (z * z2)
hence z1 / z2 = (z * z1) / (z * z2) ; :: thesis: verum