let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n holds
( x1 = x2 iff x1 - x2 = 0* n )
let x1, x2 be Element of REAL n; :: thesis: ( x1 = x2 iff x1 - x2 = 0* n )
thus ( x1 = x2 implies x1 - x2 = 0* n ) by Th7; :: thesis: ( x1 - x2 = 0* n implies x1 = x2 )
assume x1 - x2 = 0* n ; :: thesis: x1 = x2
hence x1 = x2 + (0* n) by Th11
.= x2 by EUCLID_4:1 ;
:: thesis: verum