:: deftheorem Def1 defines Gen ANALMETR:def 1 :
for V being RealLinearSpace
for w, y being VECTOR of V holds
( Gen w,y iff ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) ) );