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