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

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

suppose G is empty ; :: thesis: F \ X is programmed FinPartState of S

then reconsider H = G as empty FinPartState of S ;
H is programmed ;
hence F \ X is programmed FinPartState of S ; :: thesis: verum

end;

suppose not G is empty ; :: thesis: F \ X is programmed FinPartState of S

then reconsider G = G as non empty FinPartState of S ;
G is programmed

proof

A1: dom G c= dom F by GRFUNC_1:8;
dom F c= IL by AMI_1:def 40;
hence dom G c= IL by A1, XBOOLE_1:1; :: according to AMI_1:def 40 :: thesis: verum

end;

hence F \ X is programmed FinPartState of S ; :: thesis: verum

end;

end;