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 that
A1: Gen x,y and
A2: u = (k1 * x) + (k2 * y) ; :: thesis: ( k1 = pr1 x,y,u & k2 = pr2 x,y,u )
u = ((pr1 x,y,u) * x) + ((pr2 x,y,u) * y) by A1, Lm5;
hence ( k1 = pr1 x,y,u & k2 = pr2 x,y,u ) by A1, A2, Lm3; :: thesis: verum