let z be natural number ; :: thesis: for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for P being NAT -defined lower FinPartState of T holds
( z < card P iff il. T,z in dom P )
let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for P being NAT -defined lower FinPartState of T holds
( z < card P iff il. T,z in dom P )
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for P being NAT -defined lower FinPartState of T holds
( z < card P iff il. T,z in dom P )
let P be NAT -defined lower FinPartState of T; :: thesis: ( z < card P iff il. T,z in dom P )
deffunc H₁( Element of NAT ) -> Instruction-Location of T = il. T,$1;
defpred S₁[ Element of NAT ] means H₁($1) in dom P;
set A1 = { k where k is Element of NAT : H₁(k) in dom P } ;
set A = { k where k is Element of NAT : S₁[k] } ;

A1: now

let x be set ; :: thesis: ( x in dom P implies ex n being Element of NAT st x = H₁(n) )
assume A2: x in dom P ; :: thesis: ex n being Element of NAT st x = H₁(n)
dom P c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of T by A2, AMI_1:def 4;
consider n being natural number such that
A3: l = il. T,n by Th26;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
take n = n; :: thesis: x = H₁(n)
thus x = H₁(n) by A3; :: thesis: verum

end;

A4: for k1, k2 being Element of NAT st H₁(k1) = H₁(k2) holds
k1 = k2 by Th25;
A5: dom P,{ k where k is Element of NAT : H₁(k) in dom P } are_equipotent from FUNCT_7:sch 3(A1, A4);
A6: { k where k is Element of NAT : S₁[k] } is Subset of NAT from DOMAIN_1:sch 7();

now

let a, b be Element of NAT ; :: thesis: ( a in { k where k is Element of NAT : S₁[k] } & b < a implies b in { k where k is Element of NAT : S₁[k] } )
assume A7: a in { k where k is Element of NAT : S₁[k] } ; :: thesis: ( b < a implies b in { k where k is Element of NAT : S₁[k] } )
assume b < a ; :: thesis: b in { k where k is Element of NAT : S₁[k] }
then A8: il. T,b <= il. T,a by Th28;
ex l being Element of NAT st
( l = a & il. T,l in dom P ) by A7;
then il. T,b in dom P by A8, Def20;
hence b in { k where k is Element of NAT : S₁[k] } ; :: thesis: verum

end;

then reconsider A = { k where k is Element of NAT : S₁[k] } as Cardinal by A6, FUNCT_7:22;
A9: z is Element of NAT by ORDINAL1:def 13;
A10: ( card z = z & card (card P) = card P ) by CARD_1:def 5;
A11: card A = A by CARD_1:def 5;

hereby :: thesis: ( il. T,z in dom P implies z < card P )

assume z < card P ; :: thesis: il. T,z in dom P
then card z in card (card P) by NAT_1:42;
then z in card (dom P) by A10, CARD_1:104;
then z in card A by A5, CARD_1:21;
then ex d being Element of NAT st
( d = z & il. T,d in dom P ) by A11;
hence il. T,z in dom P ; :: thesis: verum

end;

assume il. T,z in dom P ; :: thesis: z < card P
then z in card A by A9, A11;
then z in card (dom P) by A5, CARD_1:21;
then card z in card (card P) by A10, CARD_1:104;
hence z < card P by NAT_1:42; :: thesis: verum