let r, s be Element of F_Real; :: thesis: poly_diff <%r,s%> = <%s%>
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (poly_diff <%r,s%>) . n = <%s%> . n
A1: (poly_diff <%r,s%>) . n = (<%r,s%> . (n + 1)) * (n + 1) by Def5;

per cases ( n = 0 or n <> 0 ) ;

suppose A2: n = 0 ; :: thesis: (poly_diff <%r,s%>) . n = <%s%> . n

hence (poly_diff <%r,s%>) . n = s by A1, POLYNOM5:38
.= <%s%> . n by A2, POLYNOM5:32 ;
:: thesis: verum

end;

suppose n <> 0 ; :: thesis: (poly_diff <%r,s%>) . n = <%s%> . n

then A3: 0 + 1 <= n by NAT_1:13;
1 + 1 <= n + 1 by A3, XREAL_1:6;
then <%r,s%> . (n + 1) = 0. F_Real by POLYNOM5:38;
hence (poly_diff <%r,s%>) . n = <%s%> . n by A1, A3, POLYNOM5:32; :: thesis: verum

end;

end;