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

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

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

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

end;

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

LocNums F,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 holds
ex y being set st
( y in F & S₁[x,y] )

proof

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

end;

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

proof

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

end;

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

end;

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

end;

end;