let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n, st M1 is Orthogonal holds
(M1 @ ) * M1 = M1 * (M1 @ )
let K be Field; :: thesis: for M1 being Matrix of n, st M1 is Orthogonal holds
(M1 @ ) * M1 = M1 * (M1 @ )
let M1 be Matrix of n,; :: 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