theorem Th22: :: ANPROJ_2:22

ex V being non trivial RealLinearSpace ex u, v, w, u1 being Element of V st
( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )