let k, m, n be Nat; :: thesis: for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
width (M1 ^ M2) = width M1
let D be non empty set ; :: thesis: for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
width (M1 ^ M2) = width M1
let M1 be Matrix of n,k,D; :: thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds
width (M1 ^ M2) = width M1
let M2 be Matrix of m,k,D; :: thesis: ( width M1 = width M2 implies width (M1 ^ M2) = width M1 )
assume A1: width M1 = width M2 ; :: thesis: width (M1 ^ M2) = width M1
consider n being Nat such that
A2: for x being object st x in rng (M1 ^ M2) holds
ex P being FinSequence of D st
( x = P & len P = n ) by MATRIX_0:9;

per cases ( len (M1 ^ M2) = 0 or len (M1 ^ M2) > 0 ) ;

suppose A3: len (M1 ^ M2) = 0 ; :: thesis: width (M1 ^ M2) = width M1

then (len M1) + (len M2) = 0 by FINSEQ_1:22;
then A4: len M1 = 0 ;
width (M1 ^ M2) = 0 by A3, MATRIX_0:def 3
.= width M1 by A4, MATRIX_0:def 3 ;
hence width (M1 ^ M2) = width M1 ; :: thesis: verum

end;

suppose A5: len (M1 ^ M2) > 0 ; :: thesis: width (M1 ^ M2) = width M1

then A6: (len M1) + (len M2) > 0 + 0 by FINSEQ_1:22;
consider s being FinSequence such that
A7: s in rng (M1 ^ M2) and
A8: len s = width (M1 ^ M2) by A5, MATRIX_0:def 3;
A9: ex P being FinSequence of D st
( s = P & len P = n ) by A2, A7;

per cases ( len M1 > 0 or len M2 > 0 ) by A6;

suppose len M1 > 0 ; :: thesis: width (M1 ^ M2) = width M1

then consider s1 being FinSequence such that
A10: s1 in rng M1 and
A11: len s1 = width M1 by MATRIX_0:def 3;
rng M1 c= rng (M1 ^ M2) by FINSEQ_1:29;
then ex P1 being FinSequence of D st
( s1 = P1 & len P1 = n ) by A2, A10;
hence width (M1 ^ M2) = width M1 by A8, A9, A11; :: thesis: verum

end;

suppose len M2 > 0 ; :: thesis: width (M1 ^ M2) = width M1

then consider s2 being FinSequence such that
A12: s2 in rng M2 and
A13: len s2 = width M2 by MATRIX_0:def 3;
rng M2 c= rng (M1 ^ M2) by FINSEQ_1:30;
then ex P2 being FinSequence of D st
( s2 = P2 & len P2 = n ) by A2, A12;
hence width (M1 ^ M2) = width M1 by A1, A8, A9, A13; :: thesis: verum

end;

end;

end;

end;