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 B0: n <> 0 ; :: thesis: (A * B) @ = (B @ ) * (A @ )

B1: ( len A = n & len B = n ) by MATRIX_1:25;
( width A = n & width B = n ) by MATRIX_1:25;
hence (A * B) @ = (B @ ) * (A @ ) by B0, B1, MATRIX_3:24; :: thesis: verum

end;

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

thus (A * B) @ = 1. K,n by AA4350, B0
.= (B @ ) * (A @ ) by AA4350, B0 ; :: thesis: verum

end;

end;