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_1:25;
( len B = n & width A = n ) by MATRIX_1:25;
hence (A * B) @ = (B @ ) * (A @ ) by A1, A2, MATRIX_3:24; :: 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;