let N be 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
let S be 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
let f1, f2 be sequence of NAT; ( 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 ) ) implies f1 = f2 )
assume that
A1:
f1 is bijective
and
A2:
for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,S )
and
A3:
f2 is bijective
and
A4:
for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,S )
; f1 = f2
A5:
dom f1 = NAT
by FUNCT_2:def 1;
A6:
dom f2 = NAT
by FUNCT_2:def 1;
defpred S1[ Nat] means f1 . $1 <> f2 . $1;
assume
f1 <> f2
; contradiction
then
ex c being Element of NAT st S1[c]
by FUNCT_2:63;
then A7:
ex c being Nat st S1[c]
;
consider d being Nat such that
A8:
S1[d]
and
A9:
for n being Nat st S1[n] holds
d <= n
from NAT_1:sch 5(A7);
reconsider d = d as Element of NAT by ORDINAL1:def 12;
A10:
rng f1 = NAT
by A1, FUNCT_2:def 3;
A11:
rng f2 = NAT
by A3, FUNCT_2:def 3;
consider d1 being object such that
A12:
d1 in dom f1
and
A13:
f2 . d = f1 . d1
by A10, FUNCT_1:def 3;
reconsider d1 = d1 as Element of NAT by A12;
consider d2 being object such that
A14:
d2 in dom f2
and
A15:
f1 . d = f2 . d2
by A11, FUNCT_1:def 3;
reconsider d2 = d2 as Element of NAT by A14;