let f be FinSeq-Location ; :: thesis: for I being Program of {INT,(INT *)}
for n being Element of NAT
for s being State of SCM+FSA st I +* (Start-At (0,SCM+FSA)) c= s & ( for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput ((ProgramPart s),s,n)) . f = s . f
let I be Program of {INT,(INT *)}; :: thesis: for n being Element of NAT
for s being State of SCM+FSA st I +* (Start-At (0,SCM+FSA)) c= s & ( for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput ((ProgramPart s),s,n)) . f = s . f
let n be Element of NAT ; :: thesis: for s being State of SCM+FSA st I +* (Start-At (0,SCM+FSA)) c= s & ( for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput ((ProgramPart s),s,n)) . f = s . f
let s be State of SCM+FSA; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s & ( for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I ) & not f in UsedInt*Loc I implies (Comput ((ProgramPart s),s,n)) . f = s . f )
assume that
A1: I +* (Start-At (0,SCM+FSA)) c= s and
A2: for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I and
A3: not f in UsedInt*Loc I ; :: thesis: (Comput ((ProgramPart s),s,n)) . f = s . f
defpred S₁[ Nat] means ( $1 <= n implies (Comput ((ProgramPart s),s,$1)) . f = s . f );
A4: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
set sm = Comput ((ProgramPart s),s,m);
assume A5: ( m <= n implies (Comput ((ProgramPart s),s,m)) . f = s . f ) ; :: thesis: S₁[m + 1]
assume A6: m + 1 <= n ; :: thesis: (Comput ((ProgramPart s),s,(m + 1))) . f = s . f
then m < n by NAT_1:13;
then A7: IC (Comput ((ProgramPart s),s,m)) in dom I by A2;
then A8: I . (IC (Comput ((ProgramPart s),s,m))) in rng I by FUNCT_1:def 5;
Y: (ProgramPart (Comput ((ProgramPart s),s,m))) /. (IC (Comput ((ProgramPart s),s,m))) = (Comput ((ProgramPart s),s,m)) . (IC (Comput ((ProgramPart s),s,m))) by COMPOS_1:38;
dom I misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then I c= I +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
then I c= s by A1, XBOOLE_1:1;
then I c= Comput ((ProgramPart s),s,m) by AMI_1:81;
then I . (IC (Comput ((ProgramPart s),s,m))) = (Comput ((ProgramPart s),s,m)) . (IC (Comput ((ProgramPart s),s,m))) by A7, GRFUNC_1:8;
then UsedInt*Loc ((Comput ((ProgramPart s),s,m)) . (IC (Comput ((ProgramPart s),s,m)))) c= UsedInt*Loc I by A8, Th39;
then A9: not f in UsedInt*Loc ((Comput ((ProgramPart s),s,m)) . (IC (Comput ((ProgramPart s),s,m)))) by A3;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,m)) by AMI_1:123;
thus (Comput ((ProgramPart s),s,(m + 1))) . f = (Following ((ProgramPart s),(Comput ((ProgramPart s),s,m)))) . f by EXTPRO_1:4
.= s . f by A5, A6, A9, Th70, Y, T, NAT_1:13 ; :: thesis: verum

end;

A10: S₁[ 0 ] by EXTPRO_1:3;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A10, A4);
hence (Comput ((ProgramPart s),s,n)) . f = s . f ; :: thesis: verum