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 that
A1: width A = len B and
A2: width B <> 0 ; :: thesis: (A * B) @ = (B @ ) * (A @ )
A3: len (B @ ) = width B by MATRIX_1:def 7;
len (A @ ) = width A by MATRIX_1:def 7;
then A4: width (B @ ) = len (A @ ) by A1, A2, MATRIX_2:12;
then A5: width ((B @ ) * (A @ )) = width (A @ ) by Def4;
width (A * B) > 0 by A1, A2, Def4;
then A6: width ((A * B) @ ) = len (A * B) by MATRIX_2:12
.= len A by A1, Def4 ;
A7: width ((B @ ) * (A @ )) = width (A @ ) by A4, Def4;
A8: len ((B @ ) * (A @ )) = len (B @ ) by A4, Def4
.= width B by MATRIX_1:def 7 ;
A9: len ((B @ ) * (A @ )) = len (B @ ) 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 A9, 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, A2, 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 (A @ )) = dom A by FINSEQ_1:def 3;
then A13: j in dom A by A12, ZFMISC_1:106;
then A14: Col (A @ ),j = Line A,j by MATRIX_2:16;
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;
Seg (width B) = dom (B @ ) by A3, FINSEQ_1:def 3;
then A16: i in Seg (width B) by A12, ZFMISC_1:106;
then i in Seg (width (A * B)) by A1, Def4;
then [j,i] in [:(dom (A * B)),(Seg (width (A * B))):] by A15, ZFMISC_1:106;
then A17: [j,i] in Indices (A * B) by MATRIX_1:def 5;
Line (B @ ),i = Col B,i by A16, MATRIX_2:17;
hence ((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, A17, Def4
.= ((A * B) @ ) * i,j by A17, MATRIX_1:def 7 ;
:: thesis: verum

end;

end;

end;

A18: 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, A2, 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;

len ((A * B) @ ) = width (A * B) by MATRIX_1:def 7
.= width B by A1, Def4 ;
hence (A * B) @ = (B @ ) * (A @ ) by A6, A8, A7, A10, A18, MATRIX_1:21; :: thesis: verum