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, Def7; :: thesis: verum