let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
let w, y be VECTOR of V; :: thesis: for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
let a1, a2, b1, b2 be Real; :: thesis: ( Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) implies ( a1 = b1 & a2 = b2 ) )
assume that
A1: Gen w,y and
A2: (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) ; :: thesis: ( a1 = b1 & a2 = b2 )
0. V = ((a1 * w) + (a2 * y)) - ((b1 * w) + (b2 * y)) by A2, RLVECT_1:15
.= ((a1 - b1) * w) + ((a2 - b2) * y) by Lm1 ;
then ( (- b1) + a1 = 0 & (- b2) + a2 = 0 ) by A1;
hence ( a1 = b1 & a2 = b2 ) ; :: thesis: verum