let x1 be Element of F_Complex; :: thesis: for x2 being Complex st x1 = x2 & x1 <> 0. F_Complex holds
x1 " = x2 "
let x2 be Complex; :: thesis: ( x1 = x2 & x1 <> 0. F_Complex implies x1 " = x2 " )
reconsider x4 = x2 as Element of COMPLEX by XCMPLX_0:def 2;
x4 " in COMPLEX by XCMPLX_0:def 2;
then reconsider x9 = x4 " as Element of F_Complex by Def1;
assume that
A1: x1 = x2 and
A2: x1 <> 0. F_Complex ; :: thesis: x1 " = x2 "
0c = 0. F_Complex by Def1;
then x1 * x9 = 1. F_Complex by A1, A2, Lm2, XCMPLX_0:def 7;
hence x1 " = x2 " by A2, VECTSP_1:def 10; :: thesis: verum