let N be with_zero set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: f1 = f2
A5: dom f1 = NAT by FUNCT_2:def 1;
A6: dom f2 = NAT by FUNCT_2:def 1;
defpred S₁[ Nat] means f1 . $1 <> f2 . $1;
assume f1 <> f2 ; :: thesis: contradiction
then ex c being Element of NAT st S₁[c] by FUNCT_2:63;
then A7: ex c being Nat st S₁[c] ;
consider d being Nat such that
A8: S₁[d] and
A9: for n being Nat st S₁[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;

per cases ( ( d1 <= d & d2 <= d ) or ( d <= d1 & d2 <= d ) or ( d1 <= d & d <= d2 ) or ( d <= d1 & d <= d2 ) ) ;

suppose A16: ( d1 <= d & d2 <= d ) ; :: thesis: contradiction

then f2 . d2 <= f2 . d,S by A4;
then d <= d1 by A2, A15, A13;
hence contradiction by A8, A13, A16, XXREAL_0:1; :: thesis: verum

end;

suppose A17: ( d <= d1 & d2 <= d ) ; :: thesis: contradiction

f2 . d2 = f1 . d2

proof

assume not f2 . d2 = f1 . d2 ; :: thesis: contradiction
then d <= d2 by A9;
hence contradiction by A8, A15, A17, XXREAL_0:1; :: thesis: verum

end;

hence contradiction by A1, A8, A15, A5, FUNCT_1:def 4; :: thesis: verum

end;

suppose A18: ( d1 <= d & d <= d2 ) ; :: thesis: contradiction

f1 . d1 = f2 . d1

proof

assume not f1 . d1 = f2 . d1 ; :: thesis: contradiction
then d <= d1 by A9;
hence contradiction by A8, A13, A18, XXREAL_0:1; :: thesis: verum

end;

hence contradiction by A3, A8, A13, A6, FUNCT_1:def 4; :: thesis: verum

end;

suppose A19: ( d <= d1 & d <= d2 ) ; :: thesis: contradiction

then f2 . d <= f2 . d2,S by A4;
then d1 <= d by A2, A15, A13;
hence contradiction by A8, A13, A19, XXREAL_0:1; :: thesis: verum

end;

end;