let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined lower FinPartState of holds dom F = { (il. S,k) where k is Element of NAT : k < card F }
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being NAT -defined lower FinPartState of holds dom F = { (il. S,k) where k is Element of NAT : k < card F }
let F be NAT -defined lower FinPartState of ; :: thesis: dom F = { (il. S,k) where k is Element of NAT : k < card F }
A1: dom F c= NAT by RELAT_1:def 18;

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

let x be set ; :: thesis: ( x in dom F implies x in { (il. S,k) where k is Element of NAT : k < card F } )
assume A2: x in dom F ; :: thesis: x in { (il. S,k) where k is Element of NAT : k < card F }
then reconsider f = x as Element of NAT by A1;
A3: locnum f,S < card F by A2, Th14;
reconsider i = locnum f,S as Element of NAT ;
f = il. S,i by AMISTD_1:def 13;
hence x in { (il. S,k) where k is Element of NAT : k < card F } by A3; :: thesis: verum

end;

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