let L be Field; :: thesis: for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
(canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)
let p be non-zero Polynomial of L; :: thesis: for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
(canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)
let a be Element of L; :: thesis: for b being non zero Element of L st not - (a / b) in Roots p holds
(canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)
let b be non zero Element of L; :: thesis: ( not - (a / b) in Roots p implies (canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p) )
assume A1: not - (a / b) in Roots p ; :: thesis: (canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)
set C = canFS (Roots p);
A2: Roots p = rng (canFS (Roots p)) by FUNCT_2:def 3;
then A3: (canFS (Roots p)) ^ <*(- (a / b))*> is one-to-one by A1, GRAPHSP:1;
A4: rng <*(- (a / b))*> = {(- (a / b))} by FINSEQ_1:38;
Roots <%a,b%> = {(- (a / b))} by Th10;
then Roots (<%a,b%> *' p) = (rng (canFS (Roots p))) \/ (rng <*(- (a / b))*>) by A2, A4, UPROOTS:23
.= rng ((canFS (Roots p)) ^ <*(- (a / b))*>) by FINSEQ_1:31 ;
hence (canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p) by A3, RLAFFIN3:def 1; :: thesis: verum