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;

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

end;

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

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;

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

end;

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

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