x in COMPLEX
by XCMPLX_0:def 2;

then reconsider aa = x as Element of F_Complex by COMPLFLD:def 1;

let C1, C2 be Matrix of COMPLEX; :: thesis: ( ( for ea being Element of F_Complex st ea = x holds

C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds

C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) implies C1 = C2 )

assume that

A1: for ea being Element of F_Complex st ea = x holds

C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) and

A2: for ea being Element of F_Complex st ea = x holds

C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; :: thesis: C1 = C2

C2 = Field2COMPLEX (aa * (COMPLEX2Field A)) by A2;

hence C1 = C2 by A1; :: thesis: verum

then reconsider aa = x as Element of F_Complex by COMPLFLD:def 1;

let C1, C2 be Matrix of COMPLEX; :: thesis: ( ( for ea being Element of F_Complex st ea = x holds

C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds

C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) implies C1 = C2 )

assume that

A1: for ea being Element of F_Complex st ea = x holds

C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) and

A2: for ea being Element of F_Complex st ea = x holds

C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; :: thesis: C1 = C2

C2 = Field2COMPLEX (aa * (COMPLEX2Field A)) by A2;

hence C1 = C2 by A1; :: thesis: verum