let n be Nat; :: thesis: for x0, x1, y0, y1 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds
x1 - x0 // y1 - y0
let x0, x1, y0, y1 be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds
x1 - x0 // y1 - y0
let L1, L2 be Element of line_of_REAL n; :: thesis: ( x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 implies x1 - x0 // y1 - y0 )
assume that
A1: ( x0 in L1 & x1 in L1 ) and
A2: x0 <> x1 and
A3: ( y0 in L2 & y1 in L2 ) and
A4: y0 <> y1 and
A5: L1 // L2 ; :: thesis: x1 - x0 // y1 - y0
consider x2, x3, y2, y3 being Element of REAL n such that
A6: L1 = Line (x2,x3) and
A7: L2 = Line (y2,y3) and
A8: x3 - x2 // y3 - y2 by A5;
consider t being Real such that
A9: y1 - y0 = t * (y3 - y2) by A3, A7, Th31;
A10: x1 - x0 <> 0* n by A2, Th9;
A11: y1 - y0 <> 0* n by A4, Th9;
then A12: t <> 0 by A9, EUCLID_4:3;
consider s being Real such that
A13: x1 - x0 = s * (x3 - x2) by A1, A6, Th31;
consider a being Real such that
A14: x3 - x2 = a * (y3 - y2) by A8;
x1 - x0 = (s * a) * (y3 - y2) by A13, A14, EUCLID_4:4
.= (s * a) * (1 * (y3 - y2)) by EUCLID_4:3
.= (s * a) * (((1 / t) * t) * (y3 - y2)) by A12, XCMPLX_1:106
.= (s * a) * ((1 / t) * (t * (y3 - y2))) by EUCLID_4:4
.= ((s * a) * (1 / t)) * (t * (y3 - y2)) by EUCLID_4:4
.= ((s * a) / t) * (y1 - y0) by A9, XCMPLX_1:99 ;
hence x1 - x0 // y1 - y0 by A10, A11; :: thesis: verum