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 () = {} by A2;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by ;
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 ) ;
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 ;
then A9 ^^ B9 = {} ;
hence ( A ^^ B = B & B ^^ A = B ) by A1, A4, A5; :: thesis: verum
end;
suppose A6: len A > 0 ; :: thesis: ( A ^^ B = B & B ^^ A = B )
then ( width (A9 ^^ B9) = width B & len (A9 ^^ B9) = len A ) by ;
hence A ^^ B = Segm ((A9 ^^ B9),(Seg (len A)),((Seg ()) \ (Seg ()))) by
.= B by ;
:: thesis: B ^^ A = B
( width (B9 ^^ A9) = width B & len (B9 ^^ A9) = len A ) by ;
hence B ^^ A = Segm ((B9 ^^ A9),(Seg (len A)),(Seg ())) by MATRIX13:46
.= B by Th19 ;
:: thesis: verum
end;
end;