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

end;

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;then M1 = {} ;

hence M1 ^ M2 is Matrix of n + m,k,D by A1, FINSEQ_1:34; :: thesis: verum

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;then M2 = {} ;

hence M1 ^ M2 is Matrix of n + m,k,D by A2, FINSEQ_1:34; :: thesis: verum

suppose that A3:
n <> 0
and

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

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 )

( 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;

end;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

then reconsider M3 = M1 ^ M2 as Matrix of D by MATRIX_0:9;
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;

end;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 = kend;

hence
( x = p & len p = k )
; :: thesis: verumper cases
( x in rng M1 or x in rng M2 )
by A8, XBOOLE_0:def 3;

end;

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;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

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;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

( 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 = kend;

hence
M1 ^ M2 is Matrix of n + m,k,D
by A3, A13, MATRIX_0:20; :: thesis: verumper cases
( s in rng M1 or s in rng M2 )
by A16, XBOOLE_0:def 3;

end;

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;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

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;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