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

A2: 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 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] } )
then A3: ex l being Element of NAT st
( l = a & il. (T,l) in dom P ) ;
assume b < a ; :: thesis: b in { k where k is Element of NAT : S₁[k] }
then il. (T,b) <= il. (T,a),T by Th28;
then il. (T,b) in dom P by A3, Def20;
hence b in { k where k is Element of NAT : S₁[k] } ; :: thesis: verum

end;

A4: now

let x be set ; :: thesis: ( x in dom P implies ex n being Element of NAT st x = H₁(n) )
A5: dom P c= NAT by RELAT_1:def 18;
assume x in dom P ; :: thesis: ex n being Element of NAT st x = H₁(n)
then reconsider l = x as Element of NAT by A5;
consider n being natural number such that
A6: 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 A6; :: thesis: verum

end;

reconsider A = { k where k is Element of NAT : S₁[k] } as Cardinal by A1, A2, FUNCT_7:22;
set A1 = { k where k is Element of NAT : H₁(k) in dom P } ;
A7: z is Element of NAT by ORDINAL1:def 13;
A8: card A = A by CARD_1:def 5;
A9: for k1, k2 being Element of NAT st H₁(k1) = H₁(k2) holds
k1 = k2 by Th25;
A10: dom P, { k where k is Element of NAT : H₁(k) in dom P } are_equipotent from FUNCT_7:sch 3(A4, A9);
A11: card z = z 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 A11, CARD_1:104;
then z in card A by A10, CARD_1:21;
then ex d being Element of NAT st
( d = z & il. (T,d) in dom P ) by A8;
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 A7, A8;
then z in card (dom P) by A10, CARD_1:21;
then card z in card (card P) by A11, CARD_1:104;
hence z < card P by NAT_1:42; :: thesis: verum