let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
let a be Element of R; :: thesis: h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
defpred S₁[ Nat] means for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st len p = $1 holds
h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a));
A1: S₁[ 0 ]

proof

let p be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st len p = 0 holds
h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
let a be Element of R; :: thesis: ( len p = 0 implies h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a)) )
assume A2: len p = 0 ; :: thesis: h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
then A3: p = 0_. R by POLYNOM4:5;
thus h . (eval (p,a)) = h . (eval ((0_. R),a)) by A2, POLYNOM4:5
.= h . (0. R) by POLYNOM4:17
.= 0. S by RING_2:6
.= eval ((0_. S),(h . a)) by POLYNOM4:17
.= eval (((PolyHom h) . p),(h . a)) by A3, Th23 ; :: thesis: verum

end;

A4: now :: thesis: for k being Nat st ( for m being Nat st m < k holds
S₁[m] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for m being Nat st m < k holds
S₁[m] ) implies S₁[k] )
assume A5: for m being Nat st m < k holds
S₁[m] ; :: thesis: S₁[k]

now :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st len p = k holds
h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))

let p be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st len p = k holds
h . (eval (b₂,b₃)) = eval (((PolyHom h) . b₂),(h . b₃))
let a be Element of R; :: thesis: ( len p = k implies h . (eval (b₁,b₂)) = eval (((PolyHom h) . b₁),(h . b₂)) )
assume A6: len p = k ; :: thesis: h . (eval (b₁,b₂)) = eval (((PolyHom h) . b₁),(h . b₂))

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: h . (eval (b₁,b₂)) = eval (((PolyHom h) . b₁),(h . b₂))

hence h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a)) by A6, A1; :: thesis: verum

end;

suppose k > 0 ; :: thesis: h . (eval (b₁,b₂)) = eval (((PolyHom h) . b₁),(h . b₂))

then consider q being Polynomial of R such that
A7: ( len q < len p & p = q + (LM p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) ) by A6, POLYNOM4:16;
reconsider g = q as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider LMp = LM p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider g1 = (PolyHom h) . g, g2 = (PolyHom h) . LMp as Polynomial of S ;
A8: ((PolyHom h) . g) + ((PolyHom h) . LMp) = g1 + g2 by POLYNOM3:def 10;
A9: h . (eval (q,a)) = eval (((PolyHom h) . g),(h . a)) by A6, A7, A5;
thus h . (eval (p,a)) = h . ((eval (q,a)) + (eval (LMp,a))) by A7, POLYNOM4:19
.= (h . (eval (q,a))) + (h . (eval (LMp,a))) by VECTSP_1:def 20
.= (eval (((PolyHom h) . g),(h . a))) + (eval (((PolyHom h) . LMp),(h . a))) by A9, Lm4
.= eval ((g1 + g2),(h . a)) by POLYNOM4:19
.= eval (((PolyHom h) . (g + LMp)),(h . a)) by A8, VECTSP_1:def 20
.= eval (((PolyHom h) . p),(h . a)) by A7, POLYNOM3:def 10 ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 4(A4);
ex n being Nat st n = len p ;
hence h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a)) by A10; :: thesis: verum