deffunc H₁( Element of NAT ) -> Element of NAT = $1;
let P be Program of SCM+FSA ; :: 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 )
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 l being Element of NAT st x = H₁(l) )
A2: dom P c= NAT by RELAT_1:def 18;
assume x in dom P ; :: thesis: ex l being Element of NAT st x = H₁(l)
then reconsider l = x as Element of NAT by A2;
take l = l; :: thesis: x = H₁(l)
thus x = H₁(l) ; :: thesis: verum

end;

A3: for n, m being Element of NAT st H₁(n) = H₁(m) holds
n = m ;
A4: dom P,{ m where m is Element of NAT : H₁(m) in dom P } are_equipotent from FUNCT_7:sch 3(A1, A3);
defpred S₁[ Element of NAT ] means H₁($1) in dom P;
A5: card n = n by CARD_1:def 5;
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 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 A5, CARD_1:104;
then n in card A by A4, CARD_1:21;
then ex m being Element of NAT st
( m = n & m in dom P ) by A9;
hence n in dom P ; :: thesis: verum

end;

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