let N be with_non-empty_elements set ; :: thesis:
let IL be non empty set ; :: thesis:
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis:
let f1, f2 be IL-Function of NAT ,S; :: thesis:
assume that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) and
A3: f2 is bijective and
A4: for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n ) ; :: thesis:
defpred S₁[ Nat] means f1 . $1 <> f2 . $1;
assume f1 <> f2 ; :: thesis:
then ex c being Element of NAT st S₁[c] by FUNCT_2:113;
then A5: ex c being Nat st S₁[c] ;
consider d being Nat such that
A6: S₁[d] and
A7: for n being Nat st S₁[n] holds
d <= n from NAT_1:sch 5(A5);
reconsider d = d as Element of NAT by ORDINAL1:def 13;
( f1 is onto & f2 is onto ) by A1, A3;
then A9: ( rng f1 = IL & rng f2 = IL ) by FUNCT_2:def 3;
then consider d2 being set such that
A10: ( d2 in dom f2 & f1 . d = f2 . d2 ) by FUNCT_1:def 5;
reconsider d2 = d2 as Element of NAT by A10;
consider d1 being set such that
A11: ( d1 in dom f1 & f2 . d = f1 . d1 ) by A9, FUNCT_1:def 5;
reconsider d1 = d1 as Element of NAT by A11;
A12: ( f1 is one-to-one & f2 is one-to-one ) by A1, A3;
A13: ( dom f1 = NAT & dom f2 = NAT ) by FUNCT_2:def 1;

per cases ;

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

then f2 . d2 <= f2 . d by A4;
then d <= d1 by A2, A10, A11;
hence contradiction by A6, A11, A14, XXREAL_0:1; :: thesis:

end;

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

f2 . d2 = f1 . d2

assume not f2 . d2 = f1 . d2 ; :: thesis:
then d <= d2 by A7;
hence contradiction by A6, A10, A15, XXREAL_0:1; :: thesis:

end;

hence contradiction by A6, A10, A12, A13, FUNCT_1:def 8; :: thesis:

end;

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

f1 . d1 = f2 . d1

assume not f1 . d1 = f2 . d1 ; :: thesis:
then d <= d1 by A7;
hence contradiction by A6, A11, A16, XXREAL_0:1; :: thesis:

end;

hence contradiction by A6, A11, A12, A13, FUNCT_1:def 8; :: thesis:

end;

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

then f2 . d <= f2 . d2 by A4;
then d1 <= d by A2, A10, A11;
hence contradiction by A6, A11, A17, XXREAL_0:1; :: thesis:

end;