for pm being Element of REAL
for k being Nat st k > 0 & pm <> 0 holds
GoCross_Seq_REAL (pm,k) is one-to-one