theorem Th2: :: AMI_WSTD:2

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for f1, f2 being sequence of NAT st f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,S ) ) holds
f1 = f2