let X be set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being NAT -defined FinPartState of holds F \ X is NAT -defined FinPartState of
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being NAT -defined FinPartState of holds F \ X is NAT -defined FinPartState of
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for F being NAT -defined FinPartState of holds F \ X is NAT -defined FinPartState of
let F be NAT -defined FinPartState of ; :: thesis: F \ X is NAT -defined FinPartState of
reconsider G = F \ X as FinPartState of by CARD_3:80;

per cases ( G is empty or not G is empty ) ;

suppose G is empty ; :: thesis: F \ X is NAT -defined FinPartState of

then reconsider H = G as empty FinPartState of ;
H is NAT -defined ;
hence F \ X is NAT -defined FinPartState of ; :: thesis: verum

end;

suppose not G is empty ; :: thesis: F \ X is NAT -defined FinPartState of

then reconsider G = G as non empty FinPartState of ;
A1: dom G c= dom F by GRFUNC_1:8;
dom F c= NAT by RELAT_1:def 18;
then dom G c= NAT by A1, XBOOLE_1:1;
hence F \ X is NAT -defined FinPartState of by RELAT_1:def 18; :: thesis: verum

end;

end;