let I be Program of SCM+FSA; :: thesis: ( I is InitClosed iff for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p )

hereby :: thesis: ( ( for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p ) implies I is InitClosed )

assume A1: I is InitClosed ; :: thesis: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p
let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: I is_closed_onInit s,p
A2: I c= p +* I by FUNCT_4:25;
A3: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
for k being Element of NAT holds IC (Comput ((p +* I),(Initialized s),k)) in dom I by A1, Def1, A2, A3;
hence I is_closed_onInit s,p by Def4; :: thesis: verum

end;

assume A4: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p ; :: thesis: I is InitClosed

now

let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA st I c= p holds
for k being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,k)) in dom I
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= p implies for k being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,k)) in dom I )
assume I c= p ; :: thesis: for k being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,k)) in dom I
then A5: p +* I = p by FUNCT_4:98;
let k be Element of NAT ; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies IC (Comput (p,s,k)) in dom I )
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC (Comput (p,s,k)) in dom I
then A6: s = Initialized s by FUNCT_4:98;
I is_closed_onInit s,p by A4;
hence IC (Comput (p,s,k)) in dom I by A6, Def4, A5; :: thesis: verum

end;

hence I is InitClosed by Def1; :: thesis: verum