let I be Program of SCM+FSA; :: thesis: ( I is paraclosed iff for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P )
thus ( I is paraclosed implies for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) :: thesis: ( ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) implies I is paraclosed )

proof

assume A1: I is paraclosed ; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P
let P be Instruction-Sequence of SCM+FSA; :: thesis: I is_closed_on s,P
let k be Element of NAT ; :: according to SCMFSA7B:def 6 :: thesis: IC (Comput ((P +* I),(Initialize s),k)) in dom I
I c= P +* I by FUNCT_4:25;
hence IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, AMISTD_1:def 10; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ; :: thesis: I is paraclosed
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not I c= b₁ or for b₂ being Element of NAT holds IC (Comput (b₁,s,b₂)) in K405(NAT,I) )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K405(NAT,I) )
assume A3: I c= P ; :: thesis: for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K405(NAT,I)
let n be Element of NAT ; :: thesis: IC (Comput (P,s,n)) in K405(NAT,I)
A4: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
A5: P = P +* I by A3, FUNCT_4:98;
A6: s = Initialize s by A4, FUNCT_4:98;
I is_closed_on s,P by A2;
hence IC (Comput (P,s,n)) in dom I by A5, A6, Def7; :: thesis: verum