let z, z2, z1 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 z1' = z1, z2' = z2, z' = 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:44;
thus z1 / z2 = z1' / z2' by A2, Th8
.= (z1' * z') / (z2' * z') by A1, Th9, XCMPLX_1:92
.= (z1 * z) / (z2 * z) by A3, Th8 ; :: thesis: z1 / z2 = (z * z1) / (z * z2)
hence z1 / z2 = (z * z1) / (z * z2) ; :: thesis: verum