let n be Nat; :: thesis: for x0, x1, x2, x3, y0, y1, y2, y3 being Element of REAL n st x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 holds
y1 - y0,y3 - y2 are_lindependent2
let x0, x1, x2, x3, y0, y1, y2, y3 be Element of REAL n; :: thesis: ( x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 implies y1 - y0,y3 - y2 are_lindependent2 )
assume that
A1: x1 - x0,x3 - x2 are_lindependent2 and
A2: ( y0 in Line (x0,x1) & y1 in Line (x0,x1) ) and
A3: y0 <> y1 and
A4: ( y2 in Line (x2,x3) & y3 in Line (x2,x3) ) and
A5: y2 <> y3 ; :: thesis: y1 - y0,y3 - y2 are_lindependent2
consider s being Real such that
A6: y1 - y0 = s * (x1 - x0) by A2, Th31;
consider t being Real such that
A7: y3 - y2 = t * (x3 - x2) by A4, Th31;
for a, b being Real st (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n holds
( a = 0 & b = 0 )

proof

let a, b be Real; :: thesis: ( (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n implies ( a = 0 & b = 0 ) )
assume (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n ; :: thesis: ( a = 0 & b = 0 )
then A8: 0* n = ((a * s) * (x1 - x0)) + (b * (t * (x3 - x2))) by A6, A7, EUCLID_4:4
.= ((a * s) * (x1 - x0)) + ((b * t) * (x3 - x2)) by EUCLID_4:4 ;
then A9: a * s = 0 by A1;
A10: b * t = 0 by A1, A8;
A11: b = (b * t) / t by A5, A7, Th10, XCMPLX_1:89
.= 0 by A10 ;
a = (a * s) / s by A3, A6, Th10, XCMPLX_1:89
.= 0 by A9 ;
hence ( a = 0 & b = 0 ) by A11; :: thesis: verum

end;

hence y1 - y0,y3 - y2 are_lindependent2 ; :: thesis: verum