theorem Th3:
for
V being
RealLinearSpace for
p,
q,
r being
Element of
V st ( for
w being
Element of
V ex
a,
b,
c being
Real st
w = ((a * p) + (b * q)) + (c * r) ) & ( for
a,
b,
c being
Real st
((a * p) + (b * q)) + (c * r) = 0. V holds
(
a = 0 &
b = 0 &
c = 0 ) ) holds
for
u,
u1 being
Element of
V ex
y being
Element of
V st
(
p,
q,
y are_LinDep &
u,
u1,
y are_LinDep & not
y is
zero )