let V be RealLinearSpace; :: thesis: for x, y, u being VECTOR of V
for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 x,y,u & k2 = pr2 x,y,u )
let x, y, u be VECTOR of V; :: thesis: for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 x,y,u & k2 = pr2 x,y,u )
let k1, k2 be Real; :: thesis: ( Gen x,y & u = (k1 * x) + (k2 * y) implies ( k1 = pr1 x,y,u & k2 = pr2 x,y,u ) )
assume A1: ( Gen x,y & u = (k1 * x) + (k2 * y) ) ; :: thesis: ( k1 = pr1 x,y,u & k2 = pr2 x,y,u )
then u = ((pr1 x,y,u) * x) + ((pr2 x,y,u) * y) by Lm5;
hence ( k1 = pr1 x,y,u & k2 = pr2 x,y,u ) by A1, Lm3; :: thesis: verum