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