let A, B be non degenerated Ring; :: thesis: for x being Element of B st A is Subring of B holds
Ext_eval ((1_. A),x) = 1. B
let x be Element of B; :: thesis: ( A is Subring of B implies Ext_eval ((1_. A),x) = 1. B )
assume A0: A is Subring of B ; :: thesis: Ext_eval ((1_. A),x) = 1. B
consider F being FinSequence of B such that
A1: Ext_eval ((1_. A),x) = Sum F and
A2: len F = len (1_. A) and
A3: for n being Element of NAT st n in dom F holds
F . n = (In (((1_. A) . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by Def1;
len F = 1 by A2, POLYNOM4:4;
then A4: F . 1 = (In (((1_. A) . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (In (((1_. A) . 0),B)) * ((power B) . (x,(1 -' 1))) by XREAL_1:232
.= (In ((1. A),B)) * ((power B) . (x,(1 -' 1))) by POLYNOM3:30
.= (1. B) * ((power B) . (x,(1 -' 1))) by A0, Lm5
.= (power B) . (x,0) by XREAL_1:232
.= 1_ B by GROUP_1:def 7
.= 1. B ;
Sum F = Sum <*(1. B)*> by A2, POLYNOM4:4, FINSEQ_1:40, A4
.= 1. B by RLVECT_1:44 ;
hence Ext_eval ((1_. A),x) = 1. B by A1; :: thesis: verum