let n be Nat; 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; 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; ( 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)
; ( 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)
; 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
; 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)
; verum