let R be Ring; :: thesis: for n being Nat holds ((1. (R,n)) @) ~ = 1. (R,n)
let n be Nat; :: thesis: ((1. (R,n)) @) ~ = 1. (R,n)
(1. (R,n)) @ = 1. (R,n) by Th11;
hence ((1. (R,n)) @) ~ = 1. (R,n) by Th9; :: thesis: verum