let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is Orthogonal holds
(M1 @ ) * M1 = M1 * (M1 @ )
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is Orthogonal holds
(M1 @ ) * M1 = M1 * (M1 @ )
let M1 be Matrix of n,K; :: thesis: ( M1 is Orthogonal implies (M1 @ ) * M1 = M1 * (M1 @ ) )
assume A1: M1 is Orthogonal ; :: thesis: (M1 @ ) * M1 = M1 * (M1 @ )
then (M1 @ ) * M1 = 1. K,n by Th43;
hence (M1 @ ) * M1 = M1 * (M1 @ ) by A1, Th42; :: thesis: verum