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;

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

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: now :: thesis: A * (X1 + X2) = (A * X1) + (A * X2)end;

width (B1 + B2) = width B1
by MATRIX_3:def 3;per cases
( len A = 0 or len X1 = 0 or ( len A > 0 & len X1 > 0 ) )
;

end;

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; :: thesis: verum

end;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; :: thesis: verum

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

then
width (A * X1) = 0
by A4, MATRIX_0: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;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

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