let V be RealLinearSpace; 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; 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; ( 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)
; ( 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; verum