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 A1: ( len A = len B & width A = 0 ) ; :: thesis: ( A ^^ B = B & B ^^ A = B )
set L = len A;
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;
reconsider B' = B as Matrix of len A, width B,K by A1, MATRIX_2:7;
set AB = A' ^^ B';
set BA = B' ^^ A';

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

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

then ( len (A' ^^ B') = 0 & len (B' ^^ A') = 0 ) by MATRIX_1:def 3;
then ( A' ^^ B' = {} & B' ^^ A' = {} & A = {} & B = {} ) by A1, A2;
hence ( A ^^ B = B & B ^^ A = B ) ; :: thesis: verum

end;

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

then A3: ( width (A' ^^ B') = width B & width (B' ^^ A') = width B & len (A' ^^ B') = len A & len (B' ^^ A') = len A ) by A1, MATRIX_1:24;
hence A ^^ B = Segm (A' ^^ B'),(Seg (len A)),((Seg (width B)) \ (Seg (width A))) by A1, FINSEQ_1:4, MATRIX13:46
.= B by A1, Th19 ;
:: thesis: B ^^ A = B
thus B ^^ A = Segm (B' ^^ A'),(Seg (len A)),(Seg (width B)) by A3, MATRIX13:46
.= B by Th19 ; :: thesis: verum

end;

end;