let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( (a * w) + (c * y) = (b * w) + (d * y) implies ( a = b & c = d ) )
assume (a * w) + (c * y) = (b * w) + (d * y) ; :: thesis: ( 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 ) ; :: thesis: verum