let R be non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for n being Element of NAT ex P being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st P is RingIsomorphism
let n be Element of NAT ; :: thesis: ex P being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st P is RingIsomorphism
set PN1R = Polynom-Ring (n + 1),R;
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring n,R));
set CPN1R = the carrier of (Polynom-Ring (n + 1),R);
set P = upm n,R;
A1: upm n,R is RingHomomorphism by QUOFIELD:def 21;

now

let p be set ; :: thesis: ( p in the carrier of (Polynom-Ring (n + 1),R) implies p in rng (upm n,R) )
assume p in the carrier of (Polynom-Ring (n + 1),R) ; :: thesis: p in rng (upm n,R)
then reconsider p' = p as Element of the carrier of (Polynom-Ring (n + 1),R) ;
A2: dom (upm n,R) = the carrier of (Polynom-Ring (Polynom-Ring n,R)) by FUNCT_2:def 1;
(upm n,R) . ((mpu n,R) . p') = p' by Th30;
hence p in rng (upm n,R) by A2, FUNCT_1:def 5; :: thesis: verum

end;

then the carrier of (Polynom-Ring (n + 1),R) c= rng (upm n,R) by TARSKI:def 3;
then rng (upm n,R) = the carrier of (Polynom-Ring (n + 1),R) by XBOOLE_0:def 10;
then A3: upm n,R is RingEpimorphism by A1, QUOFIELD:def 22;
upm n,R is RingMonomorphism by A1, QUOFIELD:def 23;
then upm n,R is RingIsomorphism by A3, QUOFIELD:def 24;
hence ex P being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st P is RingIsomorphism ; :: thesis: verum