set h = the Isomorphism of F1,F2;
PolyHom the Isomorphism of F1,F2 is isomorphism ;
hence Polynom-Ring F2 is Polynom-Ring F1 -isomorphic by RING_3:def 4; :: thesis: verum