let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for p being NAT -defined FinPartState of holds ProgramPart p = p
let S be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for p being NAT -defined FinPartState of holds ProgramPart p = p
let p be NAT -defined FinPartState of ; :: thesis: ProgramPart p = p
A1: dom p c= dom (ProgramPart p)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in dom (ProgramPart p) )
A2: ( dom (ProgramPart p) = (dom p) /\ NAT & dom p c= NAT ) by RELAT_1:90, RELAT_1:def 18;
assume x in dom p ; :: thesis: x in dom (ProgramPart p)
hence x in dom (ProgramPart p) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then dom (ProgramPart p) = dom p by A1, XBOOLE_0:def 10;
hence ProgramPart p = p by GRFUNC_1:9, RELAT_1:88; :: thesis: verum