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

per cases then ( len F = 0 or len F = 1 or len F = 2 ) ;

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

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

end;

suppose A5: len F = 1 ; :: thesis: Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)

then F . 1 = (In ((<%z0,z1%> . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (In ((<%z0,z1%> . 0),B)) * ((power B) . (x,(1 -' 1))) by XREAL_1:232
.= (In ((<%z0,z1%> . 0),B)) * ((power B) . (x,0)) by XREAL_1:232
.= (In (z0,B)) * ((power B) . (x,0)) by POLYNOM5:38
.= (In (z0,B)) * (1_ B) by GROUP_1:def 7
.= In (z0,B) ;
then F = <*(In (z0,B))*> by A5, FINSEQ_1:40;
hence Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((0. B) * x) by A1, RLVECT_1:44
.= (In (z0,B)) + ((In ((0. A),B)) * x) by A0, Lm5
.= (In (z0,B)) + ((In ((<%z0,z1%> . 1),B)) * x) by A2, A5, ALGSEQ_1:8
.= (In (z0,B)) + ((In (z1,B)) * x) by POLYNOM5:38 ;
:: thesis: verum

end;

suppose A6: len F = 2 ; :: thesis: Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)

then A7: F . 1 = (In ((<%z0,z1%> . (1 -' 1)),B)) * ((power B) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (In ((<%z0,z1%> . 0),B)) * ((power B) . (x,(1 -' 1))) by XREAL_1:232
.= (In ((<%z0,z1%> . 0),B)) * ((power B) . (x,0)) by XREAL_1:232
.= (In (z0,B)) * ((power B) . (x,0)) by POLYNOM5:38
.= (In (z0,B)) * (1_ B) by GROUP_1:def 7
.= In (z0,B) ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
F . 2 = (In ((<%z0,z1%> . (2 -' 1)),B)) * ((power B) . (x,(2 -' 1))) by A3, A6, FINSEQ_3:25
.= (In (z1,B)) * ((power B) . (x,1)) by A8, POLYNOM5:38
.= (In (z1,B)) * x by GROUP_1:50 ;
then F = <*(In (z0,B)),((In (z1,B)) * x)*> by A6, A7, FINSEQ_1:44;
hence Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x) by A1, RLVECT_1:45; :: thesis: verum

end;

end;