set f = PolyHom h;
A1: for o being object st o in rng (PolyHom h) holds
o in the carrier of (Polynom-Ring S) ;
now :: thesis: for o being object st o in the carrier of (Polynom-Ring S) holds
o in rng (PolyHom h)
let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring S) implies o in rng (PolyHom h) )
assume o in the carrier of (Polynom-Ring S) ; :: thesis: o in rng (PolyHom h)
then reconsider p = o as Element of the carrier of (Polynom-Ring S) ;
deffunc H1( object ) -> set = (h ") . (p . R);
A2: for o being object st o in NAT holds
H1(o) in the carrier of R
proof
let o be object ; :: thesis: ( o in NAT implies H1(o) in the carrier of R )
assume o in NAT ; :: thesis: H1(o) in the carrier of R
then reconsider i = o as Element of NAT ;
H1(i) = (h ") . (p . i) ;
hence H1(o) in the carrier of R ; :: thesis: verum
end;
consider q being Function of NAT, the carrier of R such that
A3: for x being object st x in NAT holds
q . x = H1(x) from FUNCT_2:sch 2(A2);
 ex n being Nat st
for i being Nat st i >= n holds
q . i = 0. R
proof
take n = len p; :: thesis: for i being Nat st i >= n holds
q . i = 0. R
now :: thesis: for i being Nat st i >= n holds
q . i = 0. R
let i be Nat; :: thesis: ( i >= n implies q . i = 0. R )
A4: h " is Isomorphism of S,R by RING_3:73;
assume i >= n ; :: thesis: q . i = 0. R
then p . i = 0. S by ALGSEQ_1:8;
hence q . i = (h ") . (0. S) by A3, ORDINAL1:def 12
.= 0. R by A4, RING_2:6 ;
:: thesis: verum
end;
hence for i being Nat st i >= n holds
q . i = 0. R ; :: thesis: verum
end;
then reconsider q = q as Polynomial of R by ALGSEQ_1:def 1;
reconsider q = q as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
A5: dom (PolyHom h) = the carrier of (Polynom-Ring R) by FUNCT_2:def 1;
now :: thesis: for i being Element of NAT holds ((PolyHom h) . q) . i = p . i
let i be Element of NAT ; :: thesis: ((PolyHom h) . q) . i = p . i
A6: dom (h ") = the carrier of S by FUNCT_2:def 1;
((PolyHom h) . q) . i = h . (q . i) by Def2
.= ((h ") ") . ((h ") . (p . i)) by A3
.= p . i by A6, FUNCT_1:34 ;
hence ((PolyHom h) . q) . i = p . i ; :: thesis: verum
end;
then (PolyHom h) . q = p ;
hence o in rng (PolyHom h) by A5, FUNCT_1:def 3; :: thesis: verum
end;
then PolyHom h is onto by A1, TARSKI:2;
hence PolyHom h is RingIsomorphism ; :: thesis: verum