let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being IL -defined FinPartState of S holds ProgramPart p = p
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being IL -defined FinPartState of S holds ProgramPart p = p
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p being IL -defined FinPartState of S holds ProgramPart p = p
let p be IL -defined FinPartState of S; :: 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) )
assume A2: x in dom p ; :: thesis: x in dom (ProgramPart p)
A3: dom (ProgramPart p) = (dom p) /\ IL by RELAT_1:90;
dom p c= IL by RELAT_1:def 18;
hence x in dom (ProgramPart p) by A2, A3, 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