let R be Ring; :: thesis: for S being R -homomorphic R -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)
let S be R -homomorphic R -monomorphic Ring; :: thesis: for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)
let h be Monomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: LM ((PolyHom h) . p) = (PolyHom h) . (LM p)
reconsider f = (PolyHom h) . p as Element of the carrier of (Polynom-Ring S) ;
reconsider LMp = LM p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
A1: deg f = deg p by Th32
.= (len p) - 1 ;

now :: thesis: for i being Element of NAT holds (LM f) . i = ((PolyHom h) . LMp) . i

let i be Element of NAT ; :: thesis: (LM f) . b₁ = ((PolyHom h) . LMp) . b₁

per cases ( i = (len p) -' 1 or i <> (len p) -' 1 ) ;

suppose A2: i = (len p) -' 1 ; :: thesis: (LM f) . b₁ = ((PolyHom h) . LMp) . b₁

then (LM f) . i = f . ((len p) -' 1) by A1, POLYNOM4:def 1
.= h . (p . ((len p) -' 1)) by Def2
.= h . ((LM p) . i) by A2, POLYNOM4:def 1
.= ((PolyHom h) . LMp) . i by Def2 ;
hence (LM f) . i = ((PolyHom h) . LMp) . i ; :: thesis: verum

end;

suppose A3: i <> (len p) -' 1 ; :: thesis: (LM f) . b₁ = ((PolyHom h) . LMp) . b₁

then (LM f) . i = 0. S by A1, POLYNOM4:def 1
.= h . (0. R) by RING_2:6
.= h . ((LM p) . i) by A3, POLYNOM4:def 1
.= ((PolyHom h) . LMp) . i by Def2 ;
hence (LM f) . i = ((PolyHom h) . LMp) . i ; :: thesis: verum

end;

end;

end;

hence LM ((PolyHom h) . p) = (PolyHom h) . (LM p) by FUNCT_2:63; :: thesis: verum