let R be domRing; :: thesis: for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R)
for h being R -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))
let S be domRingExtension of R; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring R)
for h being R -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))
let p be non zero Element of the carrier of (Polynom-Ring R); :: thesis: for h being R -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))
let h be R -fixing Monomorphism of S; :: thesis: h | (Roots (S,p)) is Permutation of (Roots (S,p))
set N = Roots (S,p);
reconsider g = h | (Roots (S,p)) as Function of (Roots (S,p)),S by FUNCT_2:32;
C: dom g = Roots (S,p) by FUNCT_2:def 1;
now :: thesis: for o being object st o in rng g holds
o in Roots (S,p)
let o be object ; :: thesis: ( o in rng g implies o in Roots (S,p) )
assume o in rng g ; :: thesis: o in Roots (S,p)
then consider b being object such that
B1: ( b in dom g & o = g . b ) by FUNCT_1:def 3;
reconsider b = b as Element of S by C, B1;
h . b in Roots (S,p) by B1, prm;
hence o in Roots (S,p) by B1, FUNCT_1:47; :: thesis: verum
end;
then rng g c= Roots (S,p) ;
then reconsider g = g as Function of (Roots (S,p)),(Roots (S,p)) by C, FUNCT_2:2;
E: card (Roots (S,p)) = card (Roots (S,p)) ;
A: g is one-to-one by FUNCT_1:52;
then g is onto by E, FINSEQ_4:63;
hence h | (Roots (S,p)) is Permutation of (Roots (S,p)) by A; :: thesis: verum