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
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
let p be non-zero Polynomial of L; :: thesis: for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
let a be Element of L; :: thesis: for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
let b be non zero Element of L; :: thesis: for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
set C = canFS (Roots p);
let E be Enumeration of Roots (<%a,b%> *' p); :: thesis: ( E = (canFS (Roots p)) ^ <*(- (a / b))*> implies ( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) ) )
assume A1: E = (canFS (Roots p)) ^ <*(- (a / b))*> ; :: thesis: ( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
A2: len (canFS (Roots p)) = card (Roots p) by FINSEQ_1:93;
len <*(- (a / b))*> = 1 by FINSEQ_1:39;
hence ( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) ) by A1, A2, FINSEQ_1:22, FINSEQ_1:64; :: thesis: verum