let V be RealLinearSpace; :: thesis: for w, y, u being VECTOR of V
for a, b being Real st Gen w,y & u = (a * w) + (b * y) holds
( a = pr1 w,y,u & b = pr2 w,y,u )
let w, y, u be VECTOR of V; :: thesis: for a, b being Real st Gen w,y & u = (a * w) + (b * y) holds
( a = pr1 w,y,u & b = pr2 w,y,u )
let a, b be Real; :: thesis: ( Gen w,y & u = (a * w) + (b * y) implies ( a = pr1 w,y,u & b = pr2 w,y,u ) )
assume that
A1: Gen w,y and
A2: u = (a * w) + (b * y) ; :: thesis: ( a = pr1 w,y,u & b = pr2 w,y,u )
u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y) by A1, Lm15;
hence ( a = pr1 w,y,u & b = pr2 w,y,u ) by A1, A2, Lm14; :: thesis: verum