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

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