per cases ( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) ) ;

suppose A1: n = 0 ; :: thesis: M1 ^ M2 is Matrix of n + m,k,D

then len M1 = 0 by MATRIX_0:def 2;
then M1 = {} ;
hence M1 ^ M2 is Matrix of n + m,k,D by A1, FINSEQ_1:34; :: thesis: verum

end;

suppose A2: m = 0 ; :: thesis: M1 ^ M2 is Matrix of n + m,k,D

then len M2 = 0 by MATRIX_0:def 2;
then M2 = {} ;
hence M1 ^ M2 is Matrix of n + m,k,D by A2, FINSEQ_1:34; :: thesis: verum

end;

suppose that A3: n <> 0 and
A4: m <> 0 ; :: thesis: M1 ^ M2 is Matrix of n + m,k,D

len M2 = m by MATRIX_0:def 2;
then A5: width M2 = k by A4, MATRIX_0:20;
len M1 = n by MATRIX_0:def 2;
then A6: width M1 = k by A3, MATRIX_0:20;
ex n being Nat st
for x being object st x in rng (M1 ^ M2) holds
ex p being FinSequence of D st
( x = p & len p = n )

proof

take k ; :: thesis: for x being object st x in rng (M1 ^ M2) holds
ex p being FinSequence of D st
( x = p & len p = k )
let x be object ; :: thesis: ( x in rng (M1 ^ M2) implies ex p being FinSequence of D st
( x = p & len p = k ) )
assume A7: x in rng (M1 ^ M2) ; :: thesis: ex p being FinSequence of D st
( x = p & len p = k )
rng (M1 ^ M2) c= D * by FINSEQ_1:def 4;
then reconsider p = x as FinSequence of D by A7, FINSEQ_1:def 11;
take p ; :: thesis: ( x = p & len p = k )
A8: x in (rng M1) \/ (rng M2) by A7, FINSEQ_1:31;

now :: thesis: len p = k

per cases ( x in rng M1 or x in rng M2 ) by A8, XBOOLE_0:def 3;

suppose x in rng M1 ; :: thesis: len p = k

then consider y1 being object such that
A9: y1 in dom M1 and
A10: x = M1 . y1 by FUNCT_1:def 3;
reconsider y1 = y1 as Nat by A9, FINSEQ_3:23;
x = Line (M1,y1) by A9, A10, MATRIX_0:60;
hence len p = k by A6, MATRIX_0:def 7; :: thesis: verum

end;

suppose x in rng M2 ; :: thesis: len p = k

then consider y2 being object such that
A11: y2 in dom M2 and
A12: x = M2 . y2 by FUNCT_1:def 3;
reconsider y2 = y2 as Nat by A11, FINSEQ_3:23;
x = Line (M2,y2) by A11, A12, MATRIX_0:60;
hence len p = k by A5, MATRIX_0:def 7; :: thesis: verum

end;

end;

end;

hence ( x = p & len p = k ) ; :: thesis: verum

end;

then reconsider M3 = M1 ^ M2 as Matrix of D by MATRIX_0:9;
( len M1 = n & len M2 = m ) by MATRIX_0:def 2;
then A13: len M3 = n + m by FINSEQ_1:22;
then consider s being FinSequence such that
A14: s in rng M3 and
A15: len s = width M3 by A3, MATRIX_0:def 3;
A16: s in (rng M1) \/ (rng M2) by A14, FINSEQ_1:31;

now :: thesis: width M3 = k

per cases ( s in rng M1 or s in rng M2 ) by A16, XBOOLE_0:def 3;

suppose s in rng M1 ; :: thesis: width M3 = k

then consider y1 being object such that
A17: y1 in dom M1 and
A18: s = M1 . y1 by FUNCT_1:def 3;
reconsider y1 = y1 as Nat by A17, FINSEQ_3:23;
s = Line (M1,y1) by A17, A18, MATRIX_0:60;
hence width M3 = k by A6, A15, MATRIX_0:def 7; :: thesis: verum

end;

suppose s in rng M2 ; :: thesis: width M3 = k

then consider y2 being object such that
A19: y2 in dom M2 and
A20: s = M2 . y2 by FUNCT_1:def 3;
reconsider y2 = y2 as Nat by A19, FINSEQ_3:23;
s = Line (M2,y2) by A19, A20, MATRIX_0:60;
hence width M3 = k by A5, A15, MATRIX_0:def 7; :: thesis: verum

end;

end;

end;

hence M1 ^ M2 is Matrix of n + m,k,D by A3, A13, MATRIX_0:20; :: thesis: verum

end;

end;