let n be Element of NAT ; :: thesis: for K being Field
for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @)
let K be Field; :: thesis: for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @)
let A, B be Matrix of n,K; :: thesis: (A * B) @ = (B @) * (A @)

per cases ( n <> 0 or n = 0 ) ;

suppose A1: n <> 0 ; :: thesis: (A * B) @ = (B @) * (A @)

A2: width B = n by MATRIX_0:24;
( len B = n & width A = n ) by MATRIX_0:24;
hence (A * B) @ = (B @) * (A @) by A1, A2, MATRIX_3:22; :: thesis: verum

end;

suppose A3: n = 0 ; :: thesis: (A * B) @ = (B @) * (A @)

hence (A * B) @ = 1. (K,n) by Th15
.= (B @) * (A @) by A3, Th15 ;
:: thesis: verum

end;

end;