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 y2 - y1 = a * (x2 - x1)
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 y2 - y1 = a * (x2 - x1)
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 y2 - y1 = a * (x2 - x1) )
assume y1 in Line (x1,x2) ; :: thesis: ( not y2 in Line (x1,x2) or ex a being Real st y2 - y1 = a * (x2 - x1) )
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 y2 - y1 = a * (x2 - x1)
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
take s - t ; :: thesis: y2 - y1 = (s - t) * (x2 - x1)
y2 - y1 = ((((1 - s) * x1) + (s * x2)) - ((1 - t) * x1)) - (t * x2) by A1, A2, RVSUM_1:39
.= (((s * x2) + ((1 - s) * x1)) + (- (t * x2))) + (- ((1 - t) * x1)) by RVSUM_1:15
.= (((s * x2) + (- (t * x2))) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by RVSUM_1:15
.= (((s - t) * x2) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by Th11
.= ((s - t) * x2) + (((1 - s) * x1) + (- ((1 - t) * x1))) by RVSUM_1:15
.= ((s - t) * x2) + (((1 - s) - (1 - t)) * x1) by Th11
.= ((s - t) * x2) + ((- (s - t)) * x1)
.= (s - t) * (x2 - x1) by Th12 ;
hence y2 - y1 = (s - t) * (x2 - x1) ; :: thesis: verum