let K be Field; :: thesis: for A, B being Matrix of K st len A = len B & width A = 0 holds

( A ^^ B = B & B ^^ A = B )

let A, B be Matrix of K; :: thesis: ( len A = len B & width A = 0 implies ( A ^^ B = B & B ^^ A = B ) )

assume that

A1: len A = len B and

A2: width A = 0 ; :: thesis: ( A ^^ B = B & B ^^ A = B )

A3: Seg (width A) = {} by A2;

set L = len A;

reconsider B9 = B as Matrix of len A, width B,K by A1, MATRIX_0:51;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set AB = A9 ^^ B9;

set BA = B9 ^^ A9;

( A ^^ B = B & B ^^ A = B )

let A, B be Matrix of K; :: thesis: ( len A = len B & width A = 0 implies ( A ^^ B = B & B ^^ A = B ) )

assume that

A1: len A = len B and

A2: width A = 0 ; :: thesis: ( A ^^ B = B & B ^^ A = B )

A3: Seg (width A) = {} by A2;

set L = len A;

reconsider B9 = B as Matrix of len A, width B,K by A1, MATRIX_0:51;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set AB = A9 ^^ B9;

set BA = B9 ^^ A9;

per cases
( len A = 0 or len A > 0 )
;

end;

suppose A4:
len A = 0
; :: thesis: ( A ^^ B = B & B ^^ A = B )

then
len (B9 ^^ A9) = 0
by MATRIX_0:def 2;

then A5: B9 ^^ A9 = {} ;

len (A9 ^^ B9) = 0 by A4, MATRIX_0:def 2;

then A9 ^^ B9 = {} ;

hence ( A ^^ B = B & B ^^ A = B ) by A1, A4, A5; :: thesis: verum

end;then A5: B9 ^^ A9 = {} ;

len (A9 ^^ B9) = 0 by A4, MATRIX_0:def 2;

then A9 ^^ B9 = {} ;

hence ( A ^^ B = B & B ^^ A = B ) by A1, A4, A5; :: thesis: verum

suppose A6:
len A > 0
; :: thesis: ( A ^^ B = B & B ^^ A = B )

then
( width (A9 ^^ B9) = width B & len (A9 ^^ B9) = len A )
by A2, MATRIX_0:23;

hence A ^^ B = Segm ((A9 ^^ B9),(Seg (len A)),((Seg (width B)) \ (Seg (width A)))) by A3, MATRIX13:46

.= B by A2, Th19 ;

:: thesis: B ^^ A = B

( width (B9 ^^ A9) = width B & len (B9 ^^ A9) = len A ) by A2, A6, MATRIX_0:23;

hence B ^^ A = Segm ((B9 ^^ A9),(Seg (len A)),(Seg (width B))) by MATRIX13:46

.= B by Th19 ;

:: thesis: verum

end;hence A ^^ B = Segm ((A9 ^^ B9),(Seg (len A)),((Seg (width B)) \ (Seg (width A)))) by A3, MATRIX13:46

.= B by A2, Th19 ;

:: thesis: B ^^ A = B

( width (B9 ^^ A9) = width B & len (B9 ^^ A9) = len A ) by A2, A6, MATRIX_0:23;

hence B ^^ A = Segm ((B9 ^^ A9),(Seg (len A)),(Seg (width B))) by MATRIX13:46

.= B by Th19 ;

:: thesis: verum