let L be Field; for a, c being Element of L
for b, d being non zero Element of L holds SumRoots (<%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 SumRoots (<%a,b%> *' <%c,d%>) = (- (a / b)) + (- (c / d))
let b, d be non zero Element of L; SumRoots (<%a,b%> *' <%c,d%>) = (- (a / b)) + (- (c / d))
( SumRoots <%a,b%> = - (a / b) & SumRoots <%c,d%> = - (c / d) )
by Th27;
hence
SumRoots (<%a,b%> *' <%c,d%>) = (- (a / b)) + (- (c / d))
by Th28; verum