A1: for f being Polynomial of R ex g being Polynomial of S st
for i being Nat holds g . i = h . (f . i)

proof

let f be Polynomial of R; :: thesis: ex g being Polynomial of S st
for i being Nat holds g . i = h . (f . i)
deffunc H₁( Nat) -> Element of the carrier of S = h . (f . $1);
consider q being AlgSequence of S 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 = h . (f . i)

now :: thesis: for i being Nat holds q . i = h . (f . i)

let i be Nat; :: thesis: q . b₁ = h . (f . b₁)

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

suppose i < len f ; :: thesis: q . b₁ = h . (f . b₁)

hence q . i = h . (f . i) by A2; :: thesis: verum

end;

suppose A3: i >= len f ; :: thesis: h . (f . b₁) = q . b₁

then f . i = 0. R by ALGSEQ_1:8;
hence h . (f . i) = 0. S by RING_2:6
.= q . i by A3, A2, ALGSEQ_1:8, XXREAL_0:2 ;
:: thesis: verum

end;

end;

end;

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

end;

defpred S₁[ object , object ] means ex f being Polynomial of R ex g being Polynomial of S st
( $1 = f & $2 = g & ( for i being Nat holds g . i = h . (f . i) ) );
A4: 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 S) & 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 S) & 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 S) & S₁[x,y] )
then reconsider y = x as Polynomial of R by POLYNOM3:def 10;
consider z being Polynomial of S such that
A5: for i being Nat holds z . i = h . (y . i) by A1;
take z ; :: thesis: ( z in the carrier of (Polynom-Ring S) & S₁[x,z] )
thus ( z in the carrier of (Polynom-Ring S) & S₁[x,z] ) by A5, POLYNOM3:def 10; :: thesis: verum

end;

consider F being Function of the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring S) such that
A6: for x being object st x in the carrier of (Polynom-Ring R) holds
S₁[x,F . x] from FUNCT_2:sch 1(A4);
take F ; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (F . f) . i = h . (f . i)

now :: thesis: for f being Polynomial of R
for g being Polynomial of S st g = F . f holds
for i being Nat holds g . i = h . (f . i)

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

end;

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