let I be Program of SCM+FSA; :: thesis: ( I is paraclosed iff for s being State of SCM+FSA holds I is_closed_on s )

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

assume A1: I is paraclosed ; :: thesis: for s being State of SCM+FSA holds I is_closed_on s
let s be State of SCM+FSA; :: thesis: I is_closed_on s
for k being Element of NAT holds IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A1, FUNCT_4:26, SCMFSA6B:def 2;
hence I is_closed_on s by Def7; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA holds I is_closed_on s ; :: thesis: I is paraclosed

now

let s be State of SCM+FSA; :: thesis: for k being Element of NAT st I +* (Start-At (0,SCM+FSA)) c= s holds
IC (Comput ((ProgramPart s),s,k)) in dom I
let k be Element of NAT ; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s implies IC (Comput ((ProgramPart s),s,k)) in dom I )
assume I +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: IC (Comput ((ProgramPart s),s,k)) in dom I
then A3: s = s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
I is_closed_on s by A2;
hence IC (Comput ((ProgramPart s),s,k)) in dom I by A3, Def7; :: thesis: verum

end;

hence I is paraclosed by SCMFSA6B:def 2; :: thesis: verum