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