let V be RealLinearSpace; :: thesis: for u, x, y 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 u, x, y 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