let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Nat holds IC (Comput (P,s,k)) in dom F )

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 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 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 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 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 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 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 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 Nat holds IC (Comput (P,s,k)) in dom F )
assume A3: F c= P ; :: thesis: for k being Nat holds IC (Comput (P,s,k)) in dom F
defpred S1[ Nat] means IC (Comput (P,s,\$1)) in dom F;
A4: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
reconsider t = Comput (P,s,k) as Element of product () by CARD_3:107;
set l = IC (Comput (P,s,k));
A6: IC (Following (P,t)) in NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) ;
A7: 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 ;
then NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) c= dom F by A1, A5;
hence S1[k + 1] by A6, A7; :: thesis: verum
end;
A8: S1[ 0 ] by A2;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A8, A4); :: thesis: verum
end;
assume A9: 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 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 k being 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 Nat holds IC (Comput (F,s,k)) in dom F )
assume A10: IC s in dom F ; :: thesis: for k being Nat holds IC (Comput (F,s,k)) in dom F
consider P being Instruction-Sequence of S such that
A11: F c= P by PBOOLE:145;
let k be Nat; :: thesis: IC (Comput (F,s,k)) in dom F
A12: IC (Comput (P,s,k)) in dom F by A9, A10, A11;
defpred S1[ Nat] means Comput (P,s,\$1) = Comput (F,s,\$1);
A13: S1[ 0 ] ;
A14: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A15: S1[k] ; :: thesis: S1[k + 1]
reconsider kk = k as Nat ;
A16: IC (Comput (P,s,kk)) in dom F by A9, A10, A11;
Comput (P,s,(k + 1)) = Following (P,(Comput (F,s,k))) by
.= Following (F,(Comput (F,s,k))) by
.= Comput (F,s,(k + 1)) by EXTPRO_1:3 ;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from hence IC (Comput (F,s,k)) in dom F by A12; :: thesis: verum
end;
hence F is really-closed by Th14; :: thesis: verum