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

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