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