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