let K be Field; :: thesis: for X1, A, B1, X2, B2 being Matrix of K st X1 in Solutions_of (A,B1) & X2 in Solutions_of (A,B2) & width B1 = width B2 holds
X1 + X2 in Solutions_of (A,(B1 + B2))
let X1, A, B1, X2, B2 be Matrix of K; :: thesis: ( X1 in Solutions_of (A,B1) & X2 in Solutions_of (A,B2) & width B1 = width B2 implies X1 + X2 in Solutions_of (A,(B1 + B2)) )
assume that
A1: X1 in Solutions_of (A,B1) and
A2: X2 in Solutions_of (A,B2) and
A3: width B1 = width B2 ; :: thesis: X1 + X2 in Solutions_of (A,(B1 + B2))
A4: ex Y1 being Matrix of K st
( Y1 = X1 & len Y1 = width A & width Y1 = width B1 & A * Y1 = B1 ) by A1;
A5: width (X1 + X2) = width X1 by MATRIX_3:def 3;
A6: len (X1 + X2) = len X1 by MATRIX_3:def 3;
A7: ex Y2 being Matrix of K st
( Y2 = X2 & len Y2 = width A & width Y2 = width B2 & A * Y2 = B2 ) by A2;

A8: now

per cases ( len A = 0 or len X1 = 0 or ( len A > 0 & len X1 > 0 ) ) ;

suppose A9: len A = 0 ; :: thesis: A * (X1 + X2) = (A * X1) + (A * X2)

then len (A * X1) = 0 by A4, MATRIX_3:def 4;
then A10: len ((A * X1) + (A * X2)) = 0 by MATRIX_3:def 3;
len (A * (X1 + X2)) = 0 by A4, A6, A9, MATRIX_3:def 4;
hence A * (X1 + X2) = (A * X1) + (A * X2) by A10, CARD_2:64; :: thesis: verum

end;

suppose len X1 = 0 ; :: thesis: A * (X1 + X2) = (A * X1) + (A * X2)

then width (A * X1) = 0 by A4, MATRIX_1:def 3;
then A11: ( width ((A * X1) + (A * X2)) = 0 & width (A * (X1 + X2)) = 0 ) by A4, A6, A5, MATRIX_3:def 3, MATRIX_3:def 4;
len (A * X1) = len A by A4, MATRIX_3:def 4;
then A12: len ((A * X1) + (A * X2)) = len A by MATRIX_3:def 3;
len (A * (X1 + X2)) = len A by A4, A6, MATRIX_3:def 4;
hence A * (X1 + X2) = (A * X1) + (A * X2) by A12, A11, Lm3; :: thesis: verum

end;

suppose ( len A > 0 & len X1 > 0 ) ; :: thesis: A * (X1 + X2) = (A * X1) + (A * X2)

hence A * (X1 + X2) = (A * X1) + (A * X2) by A3, A4, A7, MATRIX_4:62; :: thesis: verum

end;

end;

end;

width (B1 + B2) = width B1 by MATRIX_3:def 3;
hence X1 + X2 in Solutions_of (A,(B1 + B2)) by A4, A7, A6, A5, A8; :: thesis: verum