let V be RealLinearSpace; 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; 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; ( 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)
; ( 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; verum