let F be NAT -defined finite initial Function; :: thesis: dom F = { k where k is Element of NAT : k < card F }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : k < card F } c= dom F

let x be object ; :: thesis: ( x in dom F implies x in { k where k is Element of NAT : k < card F } )
assume A1: x in dom F ; :: thesis: x in { k where k is Element of NAT : k < card F }
then reconsider f = x as Element of NAT ;
f < card F by A1, Lm1;
hence x in { k where k is Element of NAT : k < card F } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : k < card F } or x in dom F )
assume x in { k where k is Element of NAT : k < card F } ; :: thesis: x in dom F
then ex k being Element of NAT st
( x = k & k < card F ) ;
hence x in dom F by Lm1; :: thesis: verum