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 +* (ProgramPart I)),(s +* (Initialize I)),k)) in dom I
I c= P +* I by FUNCT_4:26;
then I c= P +* (ProgramPart I) by RELAT_1:209;
hence IC (Comput ((P +* (ProgramPart I)),(s +* (Initialize I)),k)) in dom I by A1, FUNCT_4:26, 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 Initialize I 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 Initialize I 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 Initialize I c= s or IC (Comput (P,s,b₁)) in proj1 I )
let n be Element of NAT ; :: thesis: ( not Initialize I c= s or IC (Comput (P,s,n)) in proj1 I )
assume A4: Initialize I c= s ; :: thesis: IC (Comput (P,s,n)) in proj1 I
ProgramPart I c= P by A3, RELAT_1:209;
then A5: P = P +* (ProgramPart I) by FUNCT_4:79;
A6: s = s +* (Initialize I) by A4, FUNCT_4:79;
I is_closed_on s,P by A2;
hence IC (Comput (P,s,n)) in dom I by A5, A6, Def7; :: thesis: verum