let V be RealLinearSpace; :: thesis: for w, y, u being VECTOR of V st Gen w,y holds
u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y)
let w, y, u be VECTOR of V; :: thesis: ( Gen w,y implies u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y) )
assume A1: Gen w,y ; :: thesis: u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y)
then ex b being Real st u = ((pr1 w,y,u) * w) + (b * y) by Def4;
hence u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y) by A1, Def5; :: thesis: verum