let x, y be object ; :: thesis: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y implies not x <> y )
assume that
A1: x in dom (Sgm0 A) and
A2: y in dom (Sgm0 A) and
A3: (Sgm0 A) . x = (Sgm0 A) . y and
A4: x <> y ; :: thesis: contradiction
reconsider i = x, j = y as Element of NAT by A1, A2;