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

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