let M1, M2 be Matrix of COMPLEX; :: thesis: for a being Complex st len M1 = len M2 & width M1 = width M2 holds
a * (M1 + M2) = (a * M1) + (a * M2)
let a be Complex; :: thesis: ( len M1 = len M2 & width M1 = width M2 implies a * (M1 + M2) = (a * M1) + (a * M2) )
assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; :: thesis: a * (M1 + M2) = (a * M1) + (a * M2)
a in COMPLEX by XCMPLX_0:def 2;
then reconsider ea = a as Element of F_Complex by COMPLFLD:def 1;
A2: (a * M1) + (a * M2) = Field2COMPLEX ((COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M1)))) + (COMPLEX2Field (a * M2))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M2))))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) ;
a * (M1 + M2) = Field2COMPLEX (ea * (COMPLEX2Field (M1 + M2))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) by A1, Th20 ;
hence a * (M1 + M2) = (a * M1) + (a * M2) by A2; :: thesis: verum