let V be RealLinearSpace; :: thesis: for u, x, y being VECTOR of V st Gen x,y holds
u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) )
assume A1: Gen x,y ; :: thesis: u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
then consider b being Real such that
A2: u = ((pr1 (x,y,u)) * x) + (b * y) by GEOMTRAP:def 4;
thus u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) by A1, GEOMTRAP:def 5, A2; :: thesis: verum