let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
let S be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
let F be preProgram of S; :: thesis: ( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
thus ( F is really-closed implies for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) :: thesis: ( ( for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) implies F is really-closed )

proof

assume A1: F is really-closed ; :: thesis: for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F
let s be State of S; :: thesis: ( IC s in dom F implies for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
assume A2: IC s in dom F ; :: thesis: for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F
let P be Instruction-Sequence of S; :: thesis: ( F c= P implies for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
assume Z1: F c= P ; :: thesis: for k being Element of NAT holds IC (Comput (P,s,k)) in dom F
defpred S₁[ Element of NAT ] means IC (Comput (P,s,$1)) in dom F;

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
reconsider t = Comput (P,s,k) as Element of product the Object-Kind of S by CARD_3:107;
set l = IC (Comput (P,s,k));
A5: IC (Following (P,t)) in NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) ;
A6: Comput (P,s,(k + 1)) = Following (P,t) by EXTPRO_1:3;
P /. (IC (Comput (P,s,k))) = F /. (IC (Comput (P,s,k))) by A4, Z1, PARTFUN2:61;
then NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) c= dom F by A1, A4, Def17;
hence S₁[k + 1] by A5, A6; :: thesis: verum

end;

A7: S₁[ 0 ] by A2, EXTPRO_1:2;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A3); :: thesis: verum

end;

assume Z1: for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ; :: thesis: F is really-closed
for s being State of S st IC s in dom F holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F

proof

let s be State of S; :: thesis: ( IC s in dom F implies for k being Element of NAT holds IC (Comput (F,s,k)) in dom F )
assume Z2: IC s in dom F ; :: thesis: for k being Element of NAT holds IC (Comput (F,s,k)) in dom F
consider P being Instruction-Sequence of S such that
W1: F c= P by PBOOLE:145;
let k be Element of NAT ; :: thesis: IC (Comput (F,s,k)) in dom F
A: IC (Comput (P,s,k)) in dom F by Z1, Z2, W1;
defpred S₁[ Nat] means Comput (P,s,$1) = Comput (F,s,$1);
Comput (P,s,0) = s by EXTPRO_1:2
.= Comput (F,s,0) by EXTPRO_1:2 ;
then B: S₁[ 0 ] ;
C: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume Z: S₁[k] ; :: thesis: S₁[k + 1]
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
E: IC (Comput (P,s,kk)) in dom F by Z1, Z2, W1;
Comput (P,s,(k + 1)) = Following (P,(Comput (F,s,k))) by EXTPRO_1:3, Z
.= Following (F,(Comput (F,s,k))) by E, W1, PARTFUN2:61, Z
.= Comput (F,s,(k + 1)) by EXTPRO_1:3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(B, C);
hence IC (Comput (F,s,k)) in dom F by A; :: thesis: verum

end;

hence F is really-closed by Th45; :: thesis: verum