let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
let w, y be VECTOR of V; ( Gen w,y implies for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d ) )
assume A1:
Gen w,y
; for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
let a, b, c, d be Real; ( (a * w) + (c * y) = (b * w) + (d * y) implies ( a = b & c = d ) )
assume
(a * w) + (c * y) = (b * w) + (d * y)
; ( a = b & c = d )
then 0. V =
((a * w) + (c * y)) - ((b * w) + (d * y))
by RLVECT_1:15
.=
((a - b) * w) + ((c - d) * y)
by Lm6
;
then
( (- b) + a = 0 & (- d) + c = 0 )
by A1, ANALMETR:def 1;
hence
( a = b & c = d )
; verum