let i, j be Integer; :: thesis: ( uInt . i = uInt . j implies i = j )
assume uInt . i = uInt . j ; :: thesis: i = j
then ( i <= j & j <= i ) by Lm4, SURREALO:3;
hence i = j by XXREAL_0:1; :: thesis: verum