let n be Element of NAT ; :: thesis: for x1, x0, x3, x2, 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 x1, x0, x3, x2, 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 A1: ( 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 ) ; :: thesis: y1 - y0,y3 - y2 are_lindependent2
then consider s being Real such that
A2: y1 - y0 = s * (x1 - x0) by Th36;
consider t being Real such that
A3: y3 - y2 = t * (x3 - x2) by A1, Th36;
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 0* n = ((a * s) * (x1 - x0)) + (b * (t * (x3 - x2))) by A2, A3, EUCLID_4:4
.= ((a * s) * (x1 - x0)) + ((b * t) * (x3 - x2)) by EUCLID_4:4 ;
then A4: ( a * s = 0 & b * t = 0 ) by A1, Def2;
A5: a = (a * s) / s by A1, A2, Th15, XCMPLX_1:90
.= 0 by A4 ;
b = (b * t) / t by A1, A3, Th15, XCMPLX_1:90
.= 0 by A4 ;
hence ( a = 0 & b = 0 ) by A5; :: thesis: verum

end;

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