let A be Point of (TOP-REAL 2); :: thesis: for lambda being Real holds
( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
let lambda be Real; :: thesis: ( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
((- lambda) * A) `1 = (- (lambda * A)) `1 by RLVECT_1:79
.= - ((lambda * A) `1) by Th3 ;
hence ((- lambda) * A) `1 = - (lambda * (A `1)) by Th2; :: thesis: ((- lambda) * A) `2 = - (lambda * (A `2))
((- lambda) * A) `2 = (- (lambda * A)) `2 by RLVECT_1:79
.= - ((lambda * A) `2) by Th3 ;
hence ((- lambda) * A) `2 = - (lambda * (A `2)) by Th2; :: thesis: verum