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
card (Roots (<%a,b%> *' p)) = 1 + (card (Roots 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
card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p))
let a be Element of L; :: thesis: for b being non zero Element of L st not - (a / b) in Roots p holds
card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p))
let b be non zero Element of L; :: thesis: ( not - (a / b) in Roots p implies card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p)) )
A1: Roots (<%a,b%> *' p) = (Roots <%a,b%>) \/ (Roots p) by UPROOTS:23;
Roots <%a,b%> = {(- (a / b))} by Th10;
hence ( not - (a / b) in Roots p implies card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p)) ) by A1, CARD_2:41; :: thesis: verum