let L be Field; 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; 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; 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
;
verum