let z be Nat; :: thesis: for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for P being NAT -defined the InstructionsF of b₂ -valued finite lower Function holds
( z < card P iff il. (T,z) in dom P )
let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for P being NAT -defined the InstructionsF of b₁ -valued finite lower Function holds
( z < card P iff il. (T,z) in dom P )
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for P being NAT -defined the InstructionsF of T -valued finite lower Function holds
( z < card P iff il. (T,z) in dom P )
let P be NAT -defined the InstructionsF of T -valued finite lower Function; :: 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 :: thesis: for a, b being Nat st a in { k where k is Element of NAT : S₁[k] } & b < a holds
b in { k where k is Element of NAT : S₁[k] }

let a, b be 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 ) ;
A4: b in NAT by ORDINAL1:def 12;
assume b < a ; :: thesis: b in { k where k is Element of NAT : S₁[k] }
then il. (T,b) <= il. (T,a),T by Th8;
then il. (T,b) in dom P by A3, Def10;
hence b in { k where k is Element of NAT : S₁[k] } by A4; :: thesis: verum

end;

A5: now :: thesis: for x being set st x in dom P holds
ex n being Element of NAT st x = H₁(n)

let x be set ; :: thesis: ( x in dom P implies ex n being Element of NAT st x = H₁(n) )
assume x in dom P ; :: thesis: ex n being Element of NAT st x = H₁(n)
then reconsider l = x as Element of NAT ;
consider n being Nat such that
A6: l = il. (T,n) by Th6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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:20;
set A1 = { k where k is Element of NAT : H₁(k) in dom P } ;
A7: z is Element of NAT by ORDINAL1:def 12;
A8: for k1, k2 being Element of NAT st H₁(k1) = H₁(k2) holds
k1 = k2 by Th5;
A9: dom P, { k where k is Element of NAT : H₁(k) in dom P } are_equipotent from FUNCT_7:sch 3(A5, A8);

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 (Segm z) in card (Segm (card P)) by NAT_1:41;
then z in card (dom P) by CARD_1:62;
then z in card A by A9, CARD_1:5;
then ex d being Element of NAT st
( d = z & il. (T,d) in dom P ) ;
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;
then z in card (dom P) by A9, CARD_1:5;
then card (Segm z) in card (Segm (card P)) by CARD_1:62;
hence z < card P by NAT_1:41; :: thesis: verum