theorem Ah1: :: FUZNUM_1:2

for a, b being Real holds (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a = 0