let P be Program of SCMPDS ; :: thesis: for n being Nat holds
( n < card P iff n in dom P )
let n be Nat; :: thesis: ( n < card P iff n in dom P )
deffunc H₁( Element of NAT ) -> Element of NAT = $1;
set A = { m where m is Element of NAT : H₁(m) in dom P } ;

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 SCMPDS by A2, AMI_1:def 4;
reconsider n = l as Element of NAT by ORDINAL1:def 13;
take n = n; :: thesis: x = H₁(n)
thus x = H₁(n) ; :: thesis: verum

end;

A4: for n, m being Element of NAT st H₁(n) = H₁(m) holds
n = m ;
A5: dom P,{ m where m is Element of NAT : H₁(m) in dom P } are_equipotent from FUNCT_7:sch 3(A1, A4);
defpred S₁[ Element of NAT ] means H₁($1) in dom P;
set A = { m where m is Element of NAT : S₁[m] } ;
A6: { m where m is Element of NAT : S₁[m] } is Subset of NAT from DOMAIN_1:sch 7();

now

let n, m be Element of NAT ; :: thesis: ( n in { m where m is Element of NAT : S₁[m] } & m < n implies m in { m where m is Element of NAT : S₁[m] } )
assume that
A7: n in { m where m is Element of NAT : S₁[m] } and
A8: m < n ; :: thesis: m in { m where m is Element of NAT : S₁[m] }
ex l being Element of NAT st
( l = n & l in dom P ) by A7;
then m in dom P by A8, SCMNORM:def 1;
hence m in { m where m is Element of NAT : S₁[m] } ; :: thesis: verum

end;

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

hereby :: thesis: ( n in dom P implies n < card P )

assume n < card P ; :: thesis: n in dom P
then card n in card (card P) by NAT_1:42;
then n in card (dom P) by A9, CARD_1:104;
then n in card A by A5, CARD_1:21;
then ex m being Element of NAT st
( m = n & m in dom P ) by A10;
hence n in dom P ; :: thesis: verum

end;

X: n in NAT by ORDINAL1:def 13;
assume n in dom P ; :: thesis: n < card P
then n in card A by A10, X;
then n in card (dom P) by A5, CARD_1:21;
then card n in card (card P) by A9, CARD_1:104;
hence n < card P by NAT_1:42; :: thesis: verum