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 & X2 in Solutions_of A,B2 ) and
A2: width B1 = width B2 ; :: thesis: X1 + X2 in Solutions_of A,(B1 + B2)
consider Y1 being Matrix of K such that
A3: ( Y1 = X1 & len Y1 = width A & width Y1 = width B1 ) and
A4: A * Y1 = B1 by A1;
consider Y2 being Matrix of K such that
A5: ( Y2 = X2 & len Y2 = width A & width Y2 = width B2 ) and
A6: A * Y2 = B2 by A1;
A7: ( len (X1 + X2) = len X1 & width (X1 + X2) = width X1 & width (B1 + B2) = width B1 ) by MATRIX_3:def 3;

now

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

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

then A8: ( len (A * X1) = 0 & len (A * (X1 + X2)) = 0 ) by A3, A7, MATRIX_3:def 4;
then len ((A * X1) + (A * X2)) = 0 by MATRIX_3:def 3;
hence A * (X1 + X2) = (A * X1) + (A * X2) by A8, CARD_2:83; :: thesis: verum

end;

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

then ( width (A * X1) = 0 & len (A * X1) = len A ) by A3, A4, MATRIX_1:def 4, MATRIX_3:def 4;
then ( width ((A * X1) + (A * X2)) = 0 & len ((A * X1) + (A * X2)) = len A & len (A * (X1 + X2)) = len A & width (A * (X1 + X2)) = 0 ) by A3, A4, A7, MATRIX_3:def 3, MATRIX_3:def 4;
hence A * (X1 + X2) = (A * X1) + (A * X2) by 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 A2, A3, A5, MATRIX_4:62; :: thesis: verum

end;

end;

end;

hence X1 + X2 in Solutions_of A,(B1 + B2) by A3, A4, A6, A5, A7; :: thesis: verum