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