let n be Nat; :: thesis: for A, B being Matrix of n,REAL holds (A * B) @ = (B @) * (A @)
let A, B be Matrix of n,REAL; :: thesis: (A * B) @ = (B @) * (A @)
A1: len A = n by MATRIX_0:24;
A2: ( width A = n & len B = n ) by MATRIX_0:24;
A3: len (A * B) = n by MATRIX_0:24;
A4: width B = n by MATRIX_0:24;
A5: len (B @) = n by MATRIX_0:24;
then A6: len ((B @) * (A @)) = len (B @) by MATRIX_0:24;
A7: width (B @) = n by MATRIX_0:24
.= len (A @) by MATRIX_0:24 ;
A8: width (A * B) = n by MATRIX_0:24;
A9: width (A @) = n by MATRIX_0:24;
then A10: width ((B @) * (A @)) = width (A @) by MATRIX_0:24;

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

let i, j be Nat; :: thesis: ( [i,j] in Indices ((A * B) @) implies ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) )
A12: Indices ((A * B) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume A13: [i,j] in Indices ((A * B) @) ; :: thesis: ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)
then j in Seg (len (A * B)) by A3, A12, ZFMISC_1:87;
then A14: j in dom (A * B) by FINSEQ_1:def 3;
i in Seg (width (A * B)) by A8, A13, A12, ZFMISC_1:87;
then A15: [j,i] in Indices (A * B) by A14, ZFMISC_1:87;
Seg (width (A @)) = dom A by A1, A9, FINSEQ_1:def 3;
then j in dom A by A9, A13, A12, ZFMISC_1:87;
then A16: Col ((A @),j) = Line (A,j) by MATRIX_0:58;
reconsider i0 = i, j0 = j as Nat ;
A17: Seg (width B) = dom (B @) by A4, A5, FINSEQ_1:def 3;
A18: Indices ((B @) * (A @)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then [i,j] in [:(dom (B @)),(Seg (width (A @))):] by A6, A10, A13, A12, FINSEQ_3:29;
then i in Seg (width B) by A17, ZFMISC_1:87;
then Line ((B @),i) = Col (B,i) by MATRIX_0:59;
hence ((B @) * (A @)) * (i,j) = (Col (B,i0)) "*" (Line (A,j0)) by A7, A13, A12, A18, A16, MATRPROB:39
.= (A * B) * (j0,i0) by A2, A15, MATRPROB:39
.= ((A * B) @) * (i,j) by A15, MATRIX_0:def 6 ;
:: thesis: verum

end;

A19: ( len ((B @) * (A @)) = n & width ((B @) * (A @)) = n ) by MATRIX_0:24;
( len ((A * B) @) = n & width ((A * B) @) = n ) by MATRIX_0:24;
hence (A * B) @ = (B @) * (A @) by A19, A11, MATRIX_0:21; :: thesis: verum