let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let h be Homomorphism of R,S; :: thesis: for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let p, L be Element of the carrier of (Polynom-Ring R); :: thesis: ( L = LM p implies for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a)) )
assume A1: L = LM p ; :: thesis: for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let a be Element of R; :: thesis: h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

per cases ( p = 0_. R or p <> 0_. R ) ;

suppose A2: p = 0_. R ; :: thesis: h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

then A3: L = 0_. R by A1, POLYNOM4:13;
thus h . (eval ((LM p),a)) = h . (eval ((0_. R),a)) by A2, POLYNOM4:13
.= h . (0. R) by POLYNOM4:17
.= 0. S by RING_2:6
.= eval ((0_. S),(h . a)) by POLYNOM4:17
.= eval (((PolyHom h) . L),(h . a)) by A3, Th23 ; :: thesis: verum

end;

suppose A4: p <> 0_. R ; :: thesis: h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

set f = PolyHom h;
reconsider q = (PolyHom h) . L as Polynomial of S ;
consider F being FinSequence of the carrier of R such that
A5: ( eval ((LM p),a) = Sum F & len F = len (LM p) & ( for n being Element of NAT st n in dom F holds
F . n = ((LM p) . (n -' 1)) * ((power R) . (a,(n -' 1))) ) ) by POLYNOM4:def 2;
A6: Sum F = (p . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1))) by A5, POLYNOM4:22
.= ((LM p) . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1))) by POLYNOM4:def 1 ;
consider G being FinSequence of the carrier of S such that
A7: ( eval (q,(h . a)) = Sum G & len G = len q & ( for n being Element of NAT st n in dom G holds
G . n = (q . (n -' 1)) * ((power S) . ((h . a),(n -' 1))) ) ) by POLYNOM4:def 2;
A8: len q <= len L by Lm2;
A9: len G <= len F by A1, A5, A7, Lm2;
A10: len F = len p by A5, POLYNOM4:15;
then A11: len F <> 0 by A4, POLYNOM4:5;
then A12: 0 + 1 <= len F by NAT_1:13;
A13: (len p) -' 1 = (len p) - 1 by A11, A10, XREAL_0:def 2;
A15: for n being Element of NAT st n in dom G holds
n in dom F

proof

let n be Element of NAT ; :: thesis: ( n in dom G implies n in dom F )
assume n in dom G ; :: thesis: n in dom F
then ( 1 <= n & n <= len q ) by A7, FINSEQ_3:25;
then ( 1 <= n & n <= len L ) by A8, XXREAL_0:2;
hence n in dom F by A1, A5, FINSEQ_3:25; :: thesis: verum

end;

A16: for n being Element of NAT st n in dom G holds
h . (F . n) = G . n

proof

let n be Element of NAT ; :: thesis: ( n in dom G implies h . (F . n) = G . n )
assume A17: n in dom G ; :: thesis: h . (F . n) = G . n
hence h . (F . n) = h . (((LM p) . (n -' 1)) * ((power R) . (a,(n -' 1)))) by A15, A5
.= (h . (L . (n -' 1))) * (h . ((power R) . (a,(n -' 1)))) by A1, GROUP_6:def 6
.= (q . (n -' 1)) * (h . ((power R) . (a,(n -' 1)))) by Def2
.= (q . (n -' 1)) * (h . (a |^ (n -' 1))) by BINOM:def 2
.= (q . (n -' 1)) * ((h . a) |^ (n -' 1)) by Th14
.= (q . (n -' 1)) * ((power S) . ((h . a),(n -' 1))) by BINOM:def 2
.= G . n by A17, A7 ;
:: thesis: verum

end;

A18: for n being Element of NAT st n in dom G & n <> len p holds
G /. n = 0. S

proof

let n be Element of NAT ; :: thesis: ( n in dom G & n <> len p implies G /. n = 0. S )
assume A19: ( n in dom G & n <> len p ) ; :: thesis: G /. n = 0. S
then 1 <= n by FINSEQ_3:25;
then n - 1 = n -' 1 by XREAL_0:def 2;
then A20: n -' 1 <> (len p) -' 1 by A19, A13;
thus G /. n = G . n by A19, PARTFUN1:def 6
.= h . (F . n) by A16, A19
.= h . (((LM p) . (n -' 1)) * ((power R) . (a,(n -' 1)))) by A5, A19, A15
.= h . ((0. R) * ((power R) . (a,(n -' 1)))) by A20, POLYNOM4:def 1
.= 0. S by RING_2:6 ; :: thesis: verum

end;

per cases ( len G = len F or len G < len F ) by A9, XXREAL_0:1;

suppose A21: len G = len F ; :: thesis: h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

then A22: len G in dom G by A12, FINSEQ_3:25;
Sum G = G /. (len G) by A18, A21, A10, POLYNOM2:3, A12, FINSEQ_3:25
.= G . (len G) by A22, PARTFUN1:def 6
.= h . (F . (len F)) by A12, FINSEQ_3:25, A16, A21
.= h . (Sum F) by A6, FINSEQ_3:25, A12, A5, A10 ;
hence h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a)) by A5, A7; :: thesis: verum

end;

suppose A23: len G < len F ; :: thesis: h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

then 0. S = h . (L . ((len L) -' 1)) by A7, A5, A1, Lm3
.= h . (L . ((len p) -' 1)) by A1, POLYNOM4:15
.= h . (p . ((len p) -' 1)) by A1, POLYNOM4:def 1 ;
then A24: 0. S = (h . (p . ((len p) -' 1))) * (h . ((power R) . (a,((len p) -' 1))))
.= h . ((p . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1)))) by GROUP_6:def 6
.= h . (eval ((LM p),a)) by POLYNOM4:22 ;

now :: thesis: for n being Element of NAT st n in dom G holds
0. S = G . n

let n be Element of NAT ; :: thesis: ( n in dom G implies 0. S = G . n )
assume A25: n in dom G ; :: thesis: 0. S = G . n
then n in Seg (len G) by FINSEQ_1:def 3;
then n <> len p by A23, A10, FINSEQ_1:1;
hence 0. S = G /. n by A25, A18
.= G . n by A25, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a)) by A24, A7, POLYNOM3:1; :: thesis: verum

end;

end;

end;

end;