let n be Element of 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) ;
A3: y2 - y1 = ((((1 - s) * x1) + (s * x2)) - ((1 - t) * x1)) - (t * x2) by A1, A2, RVSUM_1:60
.= (((s * x2) + ((1 - s) * x1)) + (- (t * x2))) + (- ((1 - t) * x1)) by RVSUM_1:32
.= (((s * x2) + (- (t * x2))) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by RVSUM_1:32
.= (((s - t) * x2) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by Th16
.= ((s - t) * x2) + (((1 - s) * x1) + (- ((1 - t) * x1))) by RVSUM_1:32
.= ((s - t) * x2) + (((1 - s) - (1 - t)) * x1) by Th16
.= ((s - t) * x2) + ((- (s - t)) * x1)
.= (s - t) * (x2 - x1) by Th17 ;
take a = s - t; :: thesis: y2 - y1 = a * (x2 - x1)
thus y2 - y1 = a * (x2 - x1) by A3; :: thesis: verum