let L be Field; :: thesis: for a, c being Element of L
for b, d being non zero Element of L holds Roots (<%a,b%> *' <%c,d%>) = {(- (a / b)),(- (c / d))}
let a, c be Element of L; :: thesis: for b, d being non zero Element of L holds Roots (<%a,b%> *' <%c,d%>) = {(- (a / b)),(- (c / d))}
let b, d be non zero Element of L; :: thesis: Roots (<%a,b%> *' <%c,d%>) = {(- (a / b)),(- (c / d))}
( Roots <%a,b%> = {(- (a / b))} & Roots <%c,d%> = {(- (c / d))} ) by Th10;
hence {(- (a / b)),(- (c / d))} = (Roots <%a,b%>) \/ (Roots <%c,d%>) by ENUMSET1:1
.= Roots (<%a,b%> *' <%c,d%>) by UPROOTS:23 ;
:: thesis: verum