let R be 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 18;
then A2: upm (n,R) is RingMonomorphism by QUOFIELD:def 20;

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 p9 = p as Element of the carrier of (Polynom-Ring ((n + 1),R)) ;
( dom (upm (n,R)) = the carrier of (Polynom-Ring (Polynom-Ring (n,R))) & (upm (n,R)) . ((mpu (n,R)) . p9) = p9 ) by Th30, FUNCT_2:def 1;
hence p in rng (upm (n,R)) by FUNCT_1:def 3; :: 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 upm (n,R) is RingEpimorphism by A1, QUOFIELD:def 19;
then upm (n,R) is RingIsomorphism by A2, QUOFIELD:def 21;
hence ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism ; :: thesis: verum