let A, B be Ring; :: thesis: for x being Element of B
for z0 being Element of A st A is Subring of B holds
Ext_eval (<%z0%>,x) = In (z0,B)
let x be Element of B; :: thesis: for z0 being Element of A st A is Subring of B holds
Ext_eval (<%z0%>,x) = In (z0,B)
let z0 be Element of A; :: thesis: ( A is Subring of B implies Ext_eval (<%z0%>,x) = In (z0,B) )
assume A0: A is Subring of B ; :: thesis: Ext_eval (<%z0%>,x) = In (z0,B)
consider F being FinSequence of B such that
A1: Ext_eval (<%z0%>,x) = Sum F and
A2: len F = len <%z0%> and
A3: for n being Element of NAT st n in dom F holds
F . n = (In ((<%z0%> . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by Def1;

per cases ( len F = 0 or len F = 1 ) by A2, ALGSEQ_1:def 5, NAT_1:25;

suppose A4: len F = 0 ; :: thesis: Ext_eval (<%z0%>,x) = In (z0,B)

A5: z0 = <%z0%> . 0 by POLYNOM5:32
.= (0_. A) . 0 by A4, A2, POLYNOM4:5
.= 0. A by FUNCOP_1:7 ;
Ext_eval (<%z0%>,x) = Ext_eval ((0_. A),x) by A4, A2, POLYNOM4:5
.= 0. B by Th17
.= In (z0,B) by A5, A0, Lm5 ;
hence Ext_eval (<%z0%>,x) = In (z0,B) ; :: thesis: verum

end;

suppose A6: len F = 1 ; :: thesis: Ext_eval (<%z0%>,x) = In (z0,B)

then A7: F . 1 = (In ((<%z0%> . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (In ((<%z0%> . 0),B)) * ((power B) . (x,(1 -' 1))) by XREAL_1:232
.= (In ((<%z0%> . 0),B)) * ((power B) . (x,0)) by XREAL_1:232
.= (In (z0,B)) * ((power B) . (x,0)) by POLYNOM5:32
.= (In (z0,B)) * (1_ B) by GROUP_1:def 7
.= In (z0,B) ;
Ext_eval (<%z0%>,x) = Sum <*(In (z0,B))*> by A6, A7, FINSEQ_1:40, A1
.= In (z0,B) by RLVECT_1:44 ;
hence Ext_eval (<%z0%>,x) = In (z0,B) ; :: thesis: verum

end;

end;