let I be Program of SCM+FSA; :: thesis: ( I is paraclosed iff for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P )
thus ( I is paraclosed implies for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P ) :: thesis: ( ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P
let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: I is_closed_on s,P
let k be Element of NAT ; :: according to SCMFSA7B:def 7 :: thesis: IC (Comput ((P +* I),(Initialize s),k)) in dom I
yy: Start-At (0,SCM+FSA) c= Initialize s by FUNCT_4:26;
I c= P +* I by FUNCT_4:26;
hence IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, yy, SCMFSA6B:def 2; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P ; :: thesis: I is paraclosed
let s be State of SCM+FSA; :: according to SCMFSA6B:def 2 :: thesis: for b₁ being set holds
( not I c= b₁ or for b₂ being Element of NAT holds
( not Start-At (0,SCM+FSA) c= s or IC (Comput (b₁,s,b₂)) in proj1 I ) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not I c= P or for b₁ being Element of NAT holds
( not Start-At (0,SCM+FSA) c= s or IC (Comput (P,s,b₁)) in proj1 I ) )
assume A3: I c= P ; :: thesis: for b₁ being Element of NAT holds
( not Start-At (0,SCM+FSA) c= s or IC (Comput (P,s,b₁)) in proj1 I )
let n be Element of NAT ; :: thesis: ( not Start-At (0,SCM+FSA) c= s or IC (Comput (P,s,n)) in proj1 I )
assume A4: Start-At (0,SCM+FSA) c= s ; :: thesis: IC (Comput (P,s,n)) in proj1 I
A5: P = P +* I by A3, FUNCT_4:103, FUNCT_4:104;
A6: s = Initialize s by A4, FUNCT_4:103, FUNCT_4:104;
I is_closed_on s,P by A2;
hence IC (Comput (P,s,n)) in dom I by A5, A6, Def7; :: thesis: verum