let A, B be Point of (TOP-REAL 2); :: thesis: for lambda, mu being Real holds
( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
let lambda, mu be Real; :: thesis: ( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
((lambda * A) - (mu * B)) `1 = ((lambda * A) `1) - ((mu * B) `1) by EUCLID_6:41
.= (lambda * (A `1)) - ((mu * B) `1) by Th2 ;
hence ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) by Th2; :: thesis: ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2))
((lambda * A) - (mu * B)) `2 = ((lambda * A) `2) - ((mu * B) `2) by EUCLID_6:41
.= (lambda * (A `2)) - ((mu * B) `2) by Th2 ;
hence ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) by Th2; :: thesis: verum