set PRI = Polynom-Ring INT.Ring;
set PRR = Polynom-Ring F_Real;
let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); for x being Element of INT.Ring
for x1 being Element of F_Real st x = x1 holds
eval ((^ F),x1) = eval (F,x)
let x be Element of INT.Ring; for x1 being Element of F_Real st x = x1 holds
eval ((^ F),x1) = eval (F,x)
let x1 be Element of F_Real; ( x = x1 implies eval ((^ F),x1) = eval (F,x) )
assume A1:
x = x1
; eval ((^ F),x1) = eval (F,x)
A2: dom (eval ((^ F),x1)) =
dom (^ F)
by Def8
.=
dom F
by Def7
;
A3:
dom (eval ((^ F),x1)) = dom (^ F)
by Def8;
for i being Nat st i in dom (eval ((^ F),x1)) holds
(eval ((^ F),x1)) . i = (eval (F,x)) . i
proof
let i be
Nat;
( i in dom (eval ((^ F),x1)) implies (eval ((^ F),x1)) . i = (eval (F,x)) . i )
assume A4:
i in dom (eval ((^ F),x1))
;
(eval ((^ F),x1)) . i = (eval (F,x)) . i
then
F . i in rng F
by A2, FUNCT_1:3;
then reconsider Fi =
F . i as
Element of the
carrier of
(Polynom-Ring INT.Ring) ;
A5:
(^ F) /. i =
(^ F) . i
by A3, A4, PARTFUN1:def 6
.=
^ (F /. i)
by A4, A2, Def7
.=
^ Fi
by A4, A2, PARTFUN1:def 6
;
reconsider rFi =
(^ F) /. i as
Element of the
carrier of
(Polynom-Ring F_Real) ;
A7:
F . i = F /. i
by A4, A2, PARTFUN1:def 6;
A8:
(eval ((^ F),x1)) . i =
eval (
(~ rFi),
x1)
by A4, A3, Def8
.=
eval (
rFi,
x1)
;
(eval (F,x)) . i =
eval (
(~ (F /. i)),
x)
by A4, A2, Def8
.=
eval (
Fi,
x)
by A7
;
hence
(eval ((^ F),x1)) . i = (eval (F,x)) . i
by A8, A1, A5, FIELD_4:27;
verum
end;
hence
eval ((^ F),x1) = eval (F,x)
by A2, Def8; verum