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
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
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
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
let a be Element of L; :: thesis: for b being non zero Element of L st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
let b be non zero Element of L; :: thesis: ( not - (a / b) in Roots p implies for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E) )
assume A1: not - (a / b) in Roots p ; :: thesis: for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
set q = <%a,b%>;
set e = <*(- (a / b))*>;
set B = BRoots (<%a,b%> *' p);
set C = canFS (Roots p);
set D = canFS (Roots (<%a,b%> *' p));
let E be Enumeration of Roots (<%a,b%> *' p); :: thesis: ( E = (canFS (Roots p)) ^ <*(- (a / b))*> implies ((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E) )
assume A2: E = (canFS (Roots p)) ^ <*(- (a / b))*> ; :: thesis: ((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
A3: dom E = Seg ((len (canFS (Roots p))) + (len <*(- (a / b))*>)) by A2, FINSEQ_1:def 7;
A4: len (canFS (Roots p)) = card (Roots p) by FINSEQ_1:93;
A5: len <*(- (a / b))*> = 1 by FINSEQ_1:40;
A6: card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p)) by A1, Th15;
A7: rng (canFS (Roots (<%a,b%> *' p))) = Roots (<%a,b%> *' p) by FUNCT_2:def 3;
A8: rng ((canFS (Roots (<%a,b%> *' p))) ") = dom (canFS (Roots (<%a,b%> *' p))) by FUNCT_1:33;
A9: dom ((canFS (Roots (<%a,b%> *' p))) ") = rng (canFS (Roots (<%a,b%> *' p))) by FUNCT_1:33;
A10: dom (canFS (Roots (<%a,b%> *' p))) = Seg (len (canFS (Roots (<%a,b%> *' p)))) by FINSEQ_1:def 3;
A11: len (canFS (Roots (<%a,b%> *' p))) = card (Roots (<%a,b%> *' p)) by FINSEQ_1:93;
A12: Roots (<%a,b%> *' p) = (Roots <%a,b%>) \/ (Roots p) by UPROOTS:23;
A13: rng (canFS (Roots p)) = Roots p by FUNCT_2:def 3;
A14: rng <*(- (a / b))*> = {(- (a / b))} by FINSEQ_1:39;
A15: Roots <%a,b%> = {(- (a / b))} by Th10;
A16: rng E = (rng (canFS (Roots p))) \/ (rng <*(- (a / b))*>) by A2, FINSEQ_1:31;
then A17: rng (((canFS (Roots (<%a,b%> *' p))) ") * E) = rng ((canFS (Roots (<%a,b%> *' p))) ") by A9, A12, A13, A14, A15, RELAT_1:28;
dom (((canFS (Roots (<%a,b%> *' p))) ") * E) = dom E by A7, A9, A12, A13, A14, A15, A16, RELAT_1:27;
then ((canFS (Roots (<%a,b%> *' p))) ") * E is Function of (dom E),(dom E) by A3, A4, A5, A6, A8, A10, A11, A17, FUNCT_2:1;
hence ((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E) by A3, A4, A5, A6, A8, A10, A11, A17, FUNCT_2:57; :: thesis: verum