let R be Ring; :: thesis: for S being Subring of R
for r being Element of R
for s being Element of S
for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
let S be Subring of R; :: thesis: for r being Element of R
for s being Element of S
for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
let r be Element of R; :: thesis: for s being Element of S
for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
let s be Element of S; :: thesis: for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
let f be Polynomial of R; :: thesis: for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
let g be Polynomial of S; :: thesis: ( r = s & f = g & r is_a_root_of f implies s is_a_root_of g )
assume that
A1: r = s and
A2: f = g and
A3: eval (f,r) = 0. R ; :: according to POLYNOM5:def 7 :: thesis: s is_a_root_of g
consider F being FinSequence of R such that
A4: eval (f,r) = Sum F and
A5: len F = len f and
A6: for n being Element of NAT st n in dom F holds
F . n = (f . (n -' 1)) * ((power R) . (r,(n -' 1))) by POLYNOM4:def 2;
A7: for n being Element of NAT st n in dom F holds
F . n = (g . (n -' 1)) * ((power S) . (s,(n -' 1)))

proof

let n be Element of NAT ; :: thesis: ( n in dom F implies F . n = (g . (n -' 1)) * ((power S) . (s,(n -' 1))) )
assume A8: n in dom F ; :: thesis: F . n = (g . (n -' 1)) * ((power S) . (s,(n -' 1)))
A9: (g . (n -' 1)) * ((power S) . (s,(n -' 1))) is Element of R by Th7;
thus F . n = (f . (n -' 1)) * ((power R) . (r,(n -' 1))) by A6, A8
.= (In ((g . (n -' 1)),R)) * ((power R) . ((In (s,R)),(n -' 1))) by A1, A2
.= In (((g . (n -' 1)) * ((power S) . (s,(n -' 1)))),R) by ALGNUM_1:11
.= (g . (n -' 1)) * ((power S) . (s,(n -' 1))) by A9 ; :: thesis: verum

end;

rng F c= the carrier of S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of S )
assume y in rng F ; :: thesis: y in the carrier of S
then consider n being object such that
A10: n in dom F and
A11: F . n = y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A10;
F . n = (g . (n -' 1)) * ((power S) . (s,(n -' 1))) by A7, A10;
hence y in the carrier of S by A11; :: thesis: verum

end;

then reconsider G = F as FinSequence of S by FINSEQ_1:def 4;
A12: len G = len g by A2, A5, Th9;
Sum G is Element of R by Th7;
then Sum G = In ((Sum G),R)
.= Sum F by ALGNUM_1:10
.= 0. S by A3, A4, C0SP1:def 3 ;
hence eval (g,s) = 0. S by A7, A12, POLYNOM4:def 2; :: according to POLYNOM5:def 7 :: thesis: verum