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