let n be Nat; :: thesis: for K being Field holds 1. (K,n) is Orthogonal
let K be Field; :: thesis: 1. (K,n) is Orthogonal
A1: (1. (K,n)) @ = 1. (K,n) by Th10;
( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by Th8;
hence 1. (K,n) is Orthogonal by A1; :: thesis: verum