let K be Field; :: thesis: for A, B1, B2, X1, X2 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 A, B1, B2, X1, X2 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: A * (X1 + X2) = (A * X1) + (A * X2) by A3, A4, A7, MATRIX_4:62;
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