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