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 ; :: 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 ; :: 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 ;
len M1 = n by MATRIX_0:def 2;
then A6: width M1 = k by ;
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 ;
take p ; :: thesis: ( x = p & len p = k )
A8: x in (rng M1) \/ (rng M2) by ;
now :: thesis: len p = k
per cases ( x in rng M1 or x in rng M2 ) by ;
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 ;
x = Line (M1,y1) by ;
hence len p = k by ; :: 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 ;
x = Line (M2,y2) by ;
hence len p = k by ; :: 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 ;
A16: s in (rng M1) \/ (rng M2) by ;
now :: thesis: width M3 = k
per cases ( s in rng M1 or s in rng M2 ) by ;
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 ;
s = Line (M1,y1) by ;
hence width M3 = k by ; :: 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 ;
s = Line (M2,y2) by ;
hence width M3 = k by ; :: thesis: verum
end;
end;
end;
hence M1 ^ M2 is Matrix of n + m,k,D by ; :: thesis: verum
end;
end;