let n be Nat; :: thesis: for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y1 - y2 = a * (x1 - x2)
let y1, y2 be Element of REAL n; :: thesis: for x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y1 - y2 = a * (x1 - x2)
let x1, x2 be Element of REAL n; :: thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies ex a being Real st y1 - y2 = a * (x1 - x2) )
assume y1 in Line (x1,x2) ; :: thesis: ( not y2 in Line (x1,x2) or ex a being Real st y1 - y2 = a * (x1 - x2) )
then consider t being Real such that
A1: y1 = ((1 - t) * x1) + (t * x2) ;
assume y2 in Line (x1,x2) ; :: thesis: ex a being Real st y1 - y2 = a * (x1 - x2)
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
take s - t ; :: thesis: y1 - y2 = (s - t) * (x1 - x2)
y1 - y2 = ((((1 - t) * x1) + (t * x2)) - ((1 - s) * x1)) - (s * x2) by A1, A2, RVSUM_1:39
.= ((((1 - t) * x1) + (- ((1 - s) * x1))) + (t * x2)) + (- (s * x2)) by Lm2
.= (((1 - t) * x1) + (- ((1 - s) * x1))) + ((t * x2) + (- (s * x2))) by FINSEQOP:28
.= (((1 - t) * x1) + ((- (1 - s)) * x1)) + ((t * x2) + (- (s * x2))) by Lm4
.= (((1 - t) * x1) + ((- (1 - s)) * x1)) + ((t * x2) + ((- s) * x2)) by Lm4
.= (((1 - t) + (- (1 - s))) * x1) + ((t * x2) + ((- s) * x2)) by RVSUM_1:50
.= (((1 - t) - (1 - s)) * x1) + ((t + (- s)) * x2) by RVSUM_1:50
.= ((s - t) * x1) + ((- (s + (- t))) * x2)
.= ((s - t) * x1) + (- ((s - t) * x2)) by Lm4
.= ((s - t) * x1) + ((s - t) * (- x2)) by Lm4
.= (s - t) * (x1 - x2) by RVSUM_1:51 ;
hence y1 - y2 = (s - t) * (x1 - x2) ; :: thesis: verum