let n be Nat; 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; ( 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
; 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;
( (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n implies ( a = 0 & b = 0 ) )
assume
(a * (y1 - y0)) + (b * (y3 - y2)) = 0* n
;
( 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;
verum
end;
hence
y1 - y0,y3 - y2 are_lindependent2
; verum