let R be non degenerated Ring; :: thesis: for S being RingExtension of R
for a being Element of S holds Ext_eval ((1_. R),a) = 1. S
let S be RingExtension of R; :: thesis: for a being Element of S holds Ext_eval ((1_. R),a) = 1. S
let a be Element of S; :: thesis: Ext_eval ((1_. R),a) = 1. S
R is Subring of S by Def1;
hence Ext_eval ((1_. R),a) = 1. S by ALGNUM_1:14; :: thesis: verum