let F, G be Function of (Polynom-Ring R),(Polynom-Ring R); :: thesis: ( ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = (i + 1) * (f . (i + 1)) ) & ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (G . f) . i = (i + 1) * (f . (i + 1)) ) implies F = G )
assume that
A10: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = (i + 1) * (f . (i + 1)) and
A11: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (G . f) . i = (i + 1) * (f . (i + 1)) ; :: 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 = (m + 1) * (p . (m + 1)) by A10
.= (G . p) . m by A11 ;
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