A1: for f being Polynomial of R ex g being Polynomial of R st
for i being Nat holds g . i = (i + 1) * (f . (i + 1))

proof

let f be Polynomial of R; :: thesis: ex g being Polynomial of R st
for i being Nat holds g . i = (i + 1) * (f . (i + 1))
deffunc H₁( Nat) -> Element of the carrier of R = ($1 + 1) * (f . ($1 + 1));
consider q being AlgSequence of R such that
A2: ( len q <= len f & ( for k being Nat st k < len f holds
q . k = H₁(k) ) ) from ALGSEQ_1:sch 1();
take q ; :: thesis: for i being Nat holds q . i = (i + 1) * (f . (i + 1))

now :: thesis: for i being Nat holds q . i = (i + 1) * (f . (i + 1))

let i be Nat; :: thesis: q . b₁ = (b₁ + 1) * (f . (b₁ + 1))

per cases ( i + 1 <= len f or i + 1 > len f ) ;

suppose A3: i + 1 <= len f ; :: thesis: q . b₁ = (b₁ + 1) * (f . (b₁ + 1))

i < i + 1 by XREAL_1:29;
then i < len f by A3, XXREAL_0:2;
hence q . i = (i + 1) * (f . (i + 1)) by A2; :: thesis: verum

end;

suppose A4: i + 1 > len f ; :: thesis: (b₁ + 1) * (f . (b₁ + 1)) = q . b₁

then A5: len q < i + 1 by A2, XXREAL_0:2;
thus (i + 1) * (f . (i + 1)) = (i + 1) * (0. R) by ALGSEQ_1:8, A4
.= 0. R by Th3
.= q . i by A5, NAT_1:13, ALGSEQ_1:8 ; :: thesis: verum

end;

end;

end;

hence for i being Nat holds q . i = (i + 1) * (f . (i + 1)) ; :: thesis: verum

end;

defpred S₁[ object , object ] means ex f, g being Polynomial of R st
( $1 = f & $2 = g & ( for i being Nat holds g . i = (i + 1) * (f . (i + 1)) ) );
A6: for x being object st x in the carrier of (Polynom-Ring R) holds
ex y being object st
( y in the carrier of (Polynom-Ring R) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring R) implies ex y being object st
( y in the carrier of (Polynom-Ring R) & S₁[x,y] ) )
assume x in the carrier of (Polynom-Ring R) ; :: thesis: ex y being object st
( y in the carrier of (Polynom-Ring R) & S₁[x,y] )
then reconsider y = x as Polynomial of R by POLYNOM3:def 10;
consider z being Polynomial of R such that
A7: for i being Nat holds z . i = (i + 1) * (y . (i + 1)) by A1;
take z ; :: thesis: ( z in the carrier of (Polynom-Ring R) & S₁[x,z] )
thus ( z in the carrier of (Polynom-Ring R) & S₁[x,z] ) by A7, POLYNOM3:def 10; :: thesis: verum

end;

consider F being Function of the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R) such that
A8: for x being object st x in the carrier of (Polynom-Ring R) holds
S₁[x,F . x] from FUNCT_2:sch 1(A6);
take F ; :: 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))

now :: thesis: for f, g being Polynomial of R st g = F . f holds
for i being Nat holds g . i = (i + 1) * (f . (i + 1))

let f, g be Polynomial of R; :: thesis: ( g = F . f implies for i being Nat holds g . i = (i + 1) * (f . (i + 1)) )
assume A9: g = F . f ; :: thesis: for i being Nat holds g . i = (i + 1) * (f . (i + 1))
let i be Nat; :: thesis: g . i = (i + 1) * (f . (i + 1))
f in the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
then S₁[f,F . f] by A8;
hence g . i = (i + 1) * (f . (i + 1)) by A9; :: thesis: verum

end;

hence for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = (i + 1) * (f . (i + 1)) ; :: thesis: verum