let I be Program of SCMPDS ; :: thesis: ( I is paraclosed iff for s being State of SCMPDS holds I is_closed_on s )
set IsI = Initialized (stop I);

hereby :: thesis: ( ( for s being State of SCMPDS holds I is_closed_on s ) implies I is paraclosed )

assume A1: I is paraclosed ; :: thesis: for s being State of SCMPDS holds I is_closed_on s
let s be State of SCMPDS ; :: thesis: I is_closed_on s
Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
then for n being Element of NAT holds IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) in dom (stop I) by A1, SCMPDS_4:def 9;
hence I is_closed_on s by Def2; :: thesis: verum

end;

assume A2: for s being State of SCMPDS holds I is_closed_on s ; :: thesis: I is paraclosed

now

let s be State of SCMPDS ; :: thesis: for k being Element of NAT st Initialized (stop I) c= s holds
IC (Comput (ProgramPart s),s,k) in dom (stop I)
let k be Element of NAT ; :: thesis: ( Initialized (stop I) c= s implies IC (Comput (ProgramPart s),s,k) in dom (stop I) )
assume Initialized (stop I) c= s ; :: thesis: IC (Comput (ProgramPart s),s,k) in dom (stop I)
then A3: s = s +* (Initialized (stop I)) by FUNCT_4:79;
I is_closed_on s by A2;
hence IC (Comput (ProgramPart s),s,k) in dom (stop I) by A3, Def2; :: thesis: verum

end;

hence I is paraclosed by SCMPDS_4:def 9; :: thesis: verum