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_1:def 3;
then M1 = {} ;
hence M1 ^ M2 is Matrix of n + m,k,D by A1, FINSEQ_1:47; :: thesis: verum

end;

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

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

end;

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

A5: n > 0 by A3;
A6: m > 0 by A4;
A7: len M1 = n by MATRIX_1:def 3;
A8: len M2 = m by MATRIX_1:def 3;
A9: width M1 = k by A5, A7, MATRIX_1:20;
A10: width M2 = k by A6, A8, MATRIX_1:20;
ex n being Nat st
for x being set 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 set st x in rng (M1 ^ M2) holds
ex p being FinSequence of D st
( x = p & len p = k )
let x be set ; :: thesis: ( x in rng (M1 ^ M2) implies ex p being FinSequence of D st
( x = p & len p = k ) )
assume A11: 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 A11, FINSEQ_1:def 11;
take p ; :: thesis: ( x = p & len p = k )
A12: x in (rng M1) \/ (rng M2) by A11, FINSEQ_1:44;

now

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

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

then consider y1 being set such that
A13: ( y1 in dom M1 & x = M1 . y1 ) by FUNCT_1:def 5;
reconsider y1 = y1 as Nat by A13, FINSEQ_3:25;
x = Line M1,y1 by A13, MATRIX_2:18;
hence len p = k by A9, MATRIX_1:def 8; :: thesis: verum

end;

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

then consider y2 being set such that
A14: ( y2 in dom M2 & x = M2 . y2 ) by FUNCT_1:def 5;
reconsider y2 = y2 as Nat by A14, FINSEQ_3:25;
x = Line M2,y2 by A14, MATRIX_2:18;
hence len p = k by A10, MATRIX_1:def 8; :: 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_1:9;
( len M1 = n & len M2 = m ) by MATRIX_1:def 3;
then A15: len M3 = n + m by FINSEQ_1:35;
then len M3 <> 0 by A3;
then A16: len M3 > 0 ;
then consider s being FinSequence such that
A17: ( s in rng M3 & len s = width M3 ) by MATRIX_1:def 4;
A18: s in (rng M1) \/ (rng M2) by A17, FINSEQ_1:44;

now

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

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

then consider y1 being set such that
A19: ( y1 in dom M1 & s = M1 . y1 ) by FUNCT_1:def 5;
reconsider y1 = y1 as Nat by A19, FINSEQ_3:25;
s = Line M1,y1 by A19, MATRIX_2:18;
hence width M3 = k by A9, A17, MATRIX_1:def 8; :: thesis: verum

end;

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

then consider y2 being set such that
A20: ( y2 in dom M2 & s = M2 . y2 ) by FUNCT_1:def 5;
reconsider y2 = y2 as Nat by A20, FINSEQ_3:25;
s = Line M2,y2 by A20, MATRIX_2:18;
hence width M3 = k by A10, A17, MATRIX_1:def 8; :: thesis: verum

end;

end;

end;

hence M1 ^ M2 is Matrix of n + m,k,D by A15, A16, MATRIX_1:20; :: thesis: verum

end;

end;