let F, G be Function of (Polynom-Ring R),(Polynom-Ring S); :: thesis: ( ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = h . (f . i) ) & ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (G . f) . i = h . (f . i) ) implies F = G )
assume that
A8: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = h . (f . i) and
A9: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (G . f) . i = h . (f . i) ; :: thesis: F = G

now :: thesis: for o being object st o in the carrier of (Polynom-Ring R) holds
F . o = G . o

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies F . o = G . o )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: F . o = G . o
then reconsider p = o as Element of the carrier of (Polynom-Ring R) ;

now :: thesis: for u being object st u in NAT holds
(F . p) . u = (G . p) . u

let u be object ; :: thesis: ( u in NAT implies (F . p) . u = (G . p) . u )
assume u in NAT ; :: thesis: (F . p) . u = (G . p) . u
then reconsider m = u as Nat ;
(F . p) . m = h . (p . m) by A8
.= (G . p) . m by A9 ;
hence (F . p) . u = (G . p) . u ; :: thesis: verum

end;

then F . p = G . p ;
hence F . o = G . o ; :: thesis: verum

end;

hence F = G ; :: thesis: verum