x in COMPLEX by XCMPLX_0:def 2;
then reconsider aa = x as Element of F_Complex by COMPLFLD:def 1;
set C = Field2COMPLEX (aa * (COMPLEX2Field A));
for ea being Element of F_Complex st ea = x holds
Field2COMPLEX (aa * (COMPLEX2Field A)) = Field2COMPLEX (ea * (COMPLEX2Field A)) ;
hence ex b₁ being Matrix of COMPLEX st
for ea being Element of F_Complex st ea = x holds
b₁ = Field2COMPLEX (ea * (COMPLEX2Field A)) ; :: thesis: verum