let A, B be Ring; 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; 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; ( A is Subring of B implies Ext_eval (<%z0%>,x) = In (z0,B) )
assume A0:
A is Subring of B
; 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
;
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)
;
verum end; suppose A6:
len F = 1
;
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)
;
verum end; end;