let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being Subset of NAT holds F, LocNums F,S are_equipotent
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for F being Subset of NAT holds F, LocNums F,S are_equipotent
let F be Subset of NAT ; :: thesis: F, LocNums F,S are_equipotent

per cases ( F is empty or not F is empty ) ;

suppose F is empty ; :: thesis: F, LocNums F,S are_equipotent

then reconsider F = F as empty Subset of NAT ;
LocNums F,S is empty ;
hence F, LocNums F,S are_equipotent ; :: thesis: verum

end;

suppose A1: not F is empty ; :: thesis: F, LocNums F,S are_equipotent

LocNums F,S,F are_equipotent

proof

defpred S₁[ set , set ] means ex n being Element of NAT st
( n = $1 & $2 = il. S,n );
A2: for x being set st x in LocNums F,S holds
ex y being set st
( y in F & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in LocNums F,S implies ex y being set st
( y in F & S₁[x,y] ) )
assume x in LocNums F,S ; :: thesis: ex y being set st
( y in F & S₁[x,y] )
then consider l being Element of NAT such that
A3: x = locnum l,S and
A4: l in F ;
take l ; :: thesis: ( l in F & S₁[x,l] )
thus l in F by A4; :: thesis: S₁[x,l]
take locnum l,S ; :: thesis: ( locnum l,S = x & l = il. S,(locnum l,S) )
thus ( locnum l,S = x & l = il. S,(locnum l,S) ) by A3, AMISTD_1:def 13; :: thesis: verum

end;

consider f being Function of (LocNums F,S),F such that
A5: for x being set st x in LocNums F,S holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = LocNums F,S & proj2 f = F )
thus f is one-to-one :: thesis: ( proj1 f = LocNums F,S & proj2 f = F )

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A6: ( x in dom f & y in dom f ) and
A7: f . x = f . y ; :: thesis: x = y
dom f = LocNums F,S by A1, FUNCT_2:def 1;
then ( S₁[x,f . x] & S₁[y,f . y] ) by A5, A6;
hence x = y by A7, AMISTD_1:25; :: thesis: verum

end;

thus A8: dom f = LocNums F,S by A1, FUNCT_2:def 1; :: thesis: proj2 f = F
thus rng f c= F by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: F c= proj2 f
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in F or a in proj2 f )
assume A9: a in F ; :: thesis: a in proj2 f
then reconsider l = a as Element of NAT ;
A10: locnum l,S in dom f by A8, A9;
then S₁[ locnum l,S,f . (locnum l,S)] by A5, A8;
then f . (locnum l,S) = a by AMISTD_1:def 13;
hence a in proj2 f by A10, FUNCT_1:def 5; :: thesis: verum

end;

hence F, LocNums F,S are_equipotent ; :: thesis: verum

end;

end;