let n be Nat; :: thesis: for K being Field holds ((1. (K,n)) ~) ~ = 1. (K,n)
let K be Field; :: thesis: ((1. (K,n)) ~) ~ = 1. (K,n)
(1. (K,n)) ~ = 1. (K,n) by Th8;
hence ((1. (K,n)) ~) ~ = 1. (K,n) ; :: thesis: verum