let F be Field; :: thesis: for E being FieldExtension of F
for h being F -fixing Monomorphism of E
for p being non zero Element of the carrier of (Polynom-Ring F) holds h .: (Roots (E,p)) = Roots (E,p)
let E be FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E
for p being non zero Element of the carrier of (Polynom-Ring F) holds h .: (Roots (E,p)) = Roots (E,p)
let h be F -fixing Monomorphism of E; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds h .: (Roots (E,p)) = Roots (E,p)
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: h .: (Roots (E,p)) = Roots (E,p)
reconsider g = h | (Roots (E,p)) as bijective Function of (Roots (E,p)),(Roots (E,p)) by FIELD_8:39;
A: g is onto ;

Y: now :: thesis: for o being object st o in Roots (E,p) holds
o in h .: (Roots (E,p))

let o be object ; :: thesis: ( o in Roots (E,p) implies o in h .: (Roots (E,p)) )
assume o in Roots (E,p) ; :: thesis: o in h .: (Roots (E,p))
then consider b being object such that
C: ( b in dom (h | (Roots (E,p))) & (h | (Roots (E,p))) . b = o ) by A, FUNCT_1:def 3;
D: b in dom h by C, RELAT_1:57;
h . b = o by C, FUNCT_1:49;
hence o in h .: (Roots (E,p)) by C, D, FUNCT_1:def 6; :: thesis: verum

end;

now :: thesis: for o being object st o in h .: (Roots (E,p)) holds
o in Roots (E,p)

let o be object ; :: thesis: ( o in h .: (Roots (E,p)) implies o in Roots (E,p) )
assume o in h .: (Roots (E,p)) ; :: thesis: o in Roots (E,p)
then consider x being object such that
B: ( x in dom h & x in Roots (E,p) & o = h . x ) by FUNCT_1:def 6;
C: x in dom (h | (Roots (E,p))) by B, RELAT_1:57;
o = (h | (Roots (E,p))) . x by B, FUNCT_1:49;
hence o in Roots (E,p) by A, C, FUNCT_1:def 3; :: thesis: verum

end;

hence h .: (Roots (E,p)) = Roots (E,p) by Y, TARSKI:2; :: thesis: verum