let I be Program of SCM+FSA ; :: thesis: ( I is paraclosed implies I is InitClosed )
assume A1: I is paraclosed ; :: thesis: I is InitClosed
set SA = Start-At (insloc 0 );
A2: I +* (Start-At (insloc 0 )) c= Initialized I by Th6;

now

let s be State of SCM+FSA ; :: thesis: for n being Element of NAT st Initialized I c= s holds
IC (Computation s,n) in dom I
let n be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Computation s,n) in dom I )
assume Initialized I c= s ; :: thesis: IC (Computation s,n) in dom I
then I +* (Start-At (insloc 0 )) c= s by A2, XBOOLE_1:1;
hence IC (Computation s,n) in dom I by A1, SCMFSA6B:def 2; :: thesis: verum

end;

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