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 H1( 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 = H1(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 . b1 = (b1 + 1) * (f . (b1 + 1))
per cases ( i + 1 <= len f or i + 1 > len f ) ;
suppose A3: i + 1 <= len f ; :: thesis: q . b1 = (b1 + 1) * (f . (b1 + 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: (b1 + 1) * (f . (b1 + 1)) = q . b1
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 S1[ 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) & S1[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) & S1[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) & S1[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) & S1[x,z] )
thus ( z in the carrier of (Polynom-Ring R) & S1[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
S1[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 S1[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