let K be commutative Ring; :: 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_0:def 6;
len (A @) = width A by MATRIX_0:def 6;
then A4: width (B @) = len (A @) by A1, A2, MATRIX_0:54;
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_0:54
.= 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_0:def 6 ;
A9: len ((B @) * (A @)) = len (B @) by A4, Def4;

A10: now :: thesis: for i, j being Nat st [i,j] in Indices ((B @) * (A @)) holds
((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)

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:29;
then A12: [i,j] in [:(dom (B @)),(Seg (width (A @))):] by A5, A11;

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_0:def 3; :: thesis: verum

end;

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

then width (A @) = len A by MATRIX_0:54;
then Seg (width (A @)) = dom A by FINSEQ_1:def 3;
then A13: j in dom A by A12, ZFMISC_1:87;
then A14: Col ((A @),j) = Line (A,j) by MATRIX_0:58;
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:87;
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:87;
then A17: [j,i] in Indices (A * B) ;
Line ((B @),i) = Col (B,i) by A16, MATRIX_0:59;
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:90
.= (A * B) * (j,i) by A1, A17, Def4
.= ((A * B) @) * (i,j) by A17, MATRIX_0:def 6 ;
:: 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_0:def 3; :: thesis: verum

end;

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

hence width (A @) = len A by MATRIX_0:54; :: thesis: verum

end;

end;

end;

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