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

hereby :: thesis: ( ( for s being State of SCM+FSA holds I is_closed_onInit s ) implies I is InitClosed )

assume A1: I is InitClosed ; :: thesis: for s being State of SCM+FSA holds I is_closed_onInit s
let s be State of SCM+FSA ; :: thesis: I is_closed_onInit s
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then for k being Element of NAT holds IC (Computation (s +* (Initialized I)),k) in dom I by A1, Def1;
hence I is_closed_onInit s by Def4; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA holds I is_closed_onInit s ; :: thesis: I is InitClosed

now

let s be State of SCM+FSA ; :: thesis: for k being Element of NAT st Initialized I c= s holds
IC (Computation s,k) in dom I
let k be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Computation s,k) in dom I )
assume Initialized I c= s ; :: thesis: IC (Computation s,k) in dom I
then ( I is_closed_onInit s & s = s +* (Initialized I) ) by A2, FUNCT_4:79;
hence IC (Computation s,k) in dom I by Def4; :: thesis: verum

end;

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