consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
take V ; :: thesis: ex w, y being VECTOR of V st Gen w,y
consider u, v being VECTOR of V such that
A2: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by A1;
take u ; :: thesis: ex y being VECTOR of V st Gen u,y
take v ; :: thesis: Gen u,v
thus Gen u,v by A2, Def1; :: thesis: verum