let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for n being Nat ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism
let n be 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);
now :: thesis: for p being object st p in the carrier of (Polynom-Ring ((n + 1),R)) holds
p in rng (upm (n,R))
let p be object ; :: 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)) ;
then rng (upm (n,R)) = the carrier of (Polynom-Ring ((n + 1),R)) by XBOOLE_0:def 10;
then upm (n,R) is onto ;
then upm (n,R) is RingEpimorphism ;
then upm (n,R) is RingIsomorphism ;
hence ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism ; :: thesis: verum