let K be Field; 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; ( 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
; 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 A * (X1 + X2) = (A * X1) + (A * X2)per cases
( len A = 0 or len X1 = 0 or ( len A > 0 & len X1 > 0 ) )
;
suppose
len X1 = 0
;
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;
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; verum