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;