let K be Field; :: thesis: for A, B being Matrix of K st width A = len B & width B <> 0 holds
(A * B) @ = (B @ ) * (A @ )
let A, B be Matrix of K; :: thesis: ( width A = len B & width B <> 0 implies (A * B) @ = (B @ ) * (A @ ) )
assume A1: ( width A = len B & width B <> 0 ) ; :: thesis: (A * B) @ = (B @ ) * (A @ )
A3: ( len (B @ ) = width B & len (A @ ) = width A ) by MATRIX_1:def 7;
then A4: width (B @ ) = len (A @ ) by A1, MATRIX_2:12;
then A5: ( len ((B @ ) * (A @ )) = len (B @ ) & width ((B @ ) * (A @ )) = width (A @ ) ) by Def4;
A6: len ((A * B) @ ) = width (A * B) by MATRIX_1:def 7
.= width B by A1, Def4 ;
width (A * B) > 0 by A1, Def4;
then A7: width ((A * B) @ ) = len (A * B) by MATRIX_2:12
.= len A by A1, Def4 ;
A8: len ((B @ ) * (A @ )) = len (B @ ) by A4, Def4
.= width B by MATRIX_1:def 7 ;
A9: width ((B @ ) * (A @ )) = width (A @ ) by A4, Def4;

A10: now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((B @ ) * (A @ )) implies ((B @ ) * (A @ )) * b₁,b₂ = ((A * B) @ ) * b₁,b₂ )
assume A11: [i,j] in Indices ((B @ ) * (A @ )) ; :: thesis: ((B @ ) * (A @ )) * b₁,b₂ = ((A * B) @ ) * b₁,b₂
dom ((B @ ) * (A @ )) = dom (B @ ) by A5, FINSEQ_3:31;
then A12: [i,j] in [:(dom (B @ )),(Seg (width (A @ ))):] by A5, A11, MATRIX_1:def 5;

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

suppose width A = 0 ; :: thesis: ((B @ ) * (A @ )) * b₁,b₂ = ((A * B) @ ) * b₁,b₂

hence ((B @ ) * (A @ )) * i,j = ((A * B) @ ) * i,j by A1, MATRIX_1:def 4; :: thesis: verum

end;

suppose width A > 0 ; :: thesis: ((B @ ) * (A @ )) * b₁,b₂ = ((A * B) @ ) * b₁,b₂

then width (A @ ) = len A by MATRIX_2:12;
then ( Seg (width B) = dom (B @ ) & Seg (width (A @ )) = dom A ) by A3, FINSEQ_1:def 3;
then A13: ( i in Seg (width B) & j in dom A ) by A12, ZFMISC_1:106;
then A14: ( Line (B @ ),i = Col B,i & Col (A @ ),j = Line A,j ) by MATRIX_2:16, MATRIX_2:17;
j in Seg (len A) by A13, FINSEQ_1:def 3;
then j in Seg (len (A * B)) by A1, Def4;
then A15: j in dom (A * B) by FINSEQ_1:def 3;
i in Seg (width (A * B)) by A1, A13, Def4;
then [j,i] in [:(dom (A * B)),(Seg (width (A * B))):] by A15, ZFMISC_1:106;
then A16: [j,i] in Indices (A * B) by MATRIX_1:def 5;
thus ((B @ ) * (A @ )) * i,j = (Col B,i) "*" (Line A,j) by A4, A11, A14, Def4
.= (Line A,j) "*" (Col B,i) by FVSUM_1:115
.= (A * B) * j,i by A1, A16, Def4
.= ((A * B) @ ) * i,j by A16, MATRIX_1:def 7 ; :: thesis: verum

end;

end;

end;

width (A @ ) = len A

proof

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

suppose width A = 0 ; :: thesis: width (A @ ) = len A

hence width (A @ ) = len A by A1, MATRIX_1:def 4; :: thesis: verum

end;

suppose width A > 0 ; :: thesis: width (A @ ) = len A

hence width (A @ ) = len A by MATRIX_2:12; :: thesis: verum

end;

end;

end;

hence (A * B) @ = (B @ ) * (A @ ) by A6, A7, A8, A9, A10, MATRIX_1:21; :: thesis: verum