let a, b be Real; :: thesis: for P, Q being Element of (TOP-REAL 2) st P <> Q & ((1 - a) * P) + (a * Q) = ((1 - b) * P) + (b * Q) holds
a = b
let P, Q be Element of (TOP-REAL 2); :: thesis: ( P <> Q & ((1 - a) * P) + (a * Q) = ((1 - b) * P) + (b * Q) implies a = b )
assume that
A1: P <> Q and
A2: ((1 - a) * P) + (a * Q) = ((1 - b) * P) + (b * Q) ; :: thesis: a = b
reconsider PR2 = P, QR2 = Q as Element of REAL 2 by EUCLID:22;
reconsider R2 = ((1 - a) * PR2) + (a * QR2) as Element of (TOP-REAL 2) by EUCLID:22;

per cases ( P . 1 <> Q . 1 or P . 2 <> Q . 2 ) by A1, Th06;

suppose P . 1 <> Q . 1 ; :: thesis: a = b

then A3: (QR2 . 1) - (PR2 . 1) <> 0 ;
0 = (R2 . 1) - (R2 . 1)
.= (R2 - R2) . 1 by RVSUM_1:27
.= ((b - a) * (QR2 - PR2)) . 1 by A2, EUCLID12:1
.= (b - a) * ((QR2 - PR2) . 1) by RVSUM_1:44
.= (b - a) * ((QR2 . 1) - (PR2 . 1)) by RVSUM_1:27 ;
then b - a = 0 by A3;
hence a = b ; :: thesis: verum

end;

suppose P . 2 <> Q . 2 ; :: thesis: a = b

then A4: (QR2 . 2) - (PR2 . 2) <> 0 ;
0 = (R2 . 2) - (R2 . 2)
.= (R2 - R2) . 2 by RVSUM_1:27
.= ((b - a) * (QR2 - PR2)) . 2 by A2, EUCLID12:1
.= (b - a) * ((QR2 - PR2) . 2) by RVSUM_1:44
.= (b - a) * ((QR2 . 2) - (PR2 . 2)) by RVSUM_1:27 ;
then b - a = 0 by A4;
hence a = b ; :: thesis: verum

end;

end;