let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(),k) = Comput ((P +* (I ";" J)),(),k)

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(),k) = Comput ((P +* (I ";" J)),(),k)

let I, J be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(),k) = Comput ((P +* (I ";" J)),(),k) )

set s1 = Initialize s;
set s2 = Initialize s;
defpred S1[ Nat] means ( \$1 <= pseudo-LifeSpan (s,P,I) implies Comput ((P +* I),(),\$1) = Comput ((P +* (I ";" J)),(),\$1) );
A1: dom (P +* I) = NAT by PARTFUN1:def 2;
A2: dom (P +* (I ";" J)) = NAT by PARTFUN1:def 2;
assume A3: I is_pseudo-closed_on s,P ; :: thesis: for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(),k) = Comput ((P +* (I ";" J)),(),k)

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]
thus S1[k + 1] :: thesis: verum
proof
A6: Comput ((P +* (I ";" J)),(),(k + 1)) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k)))),(Comput ((P +* (I ";" J)),(),k))) ;
A7: Comput ((P +* I),(),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(),k)))),(Comput ((P +* I),(),k))) ;
A8: dom I c= dom (I ";" J) by SCMFSA6A:17;
A9: k + 0 < k + 1 by XREAL_1:6;
assume A10: k + 1 <= pseudo-LifeSpan (s,P,I) ; :: thesis: Comput ((P +* I),(),(k + 1)) = Comput ((P +* (I ";" J)),(),(k + 1))
then A11: k < pseudo-LifeSpan (s,P,I) by ;
then A12: IC (Comput ((P +* I),(),k)) in dom I by ;
A13: I c= P +* I by FUNCT_4:25;
A14: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A15: CurInstr ((P +* I),(Comput ((P +* I),(),k))) = (P +* I) . (IC (Comput ((P +* I),(),k))) by
.= I . (IC (Comput ((P +* I),(),k))) by ;
then I . (IC (Comput ((P +* I),(),k))) <> halt SCM+FSA by ;
then CurInstr ((P +* I),(Comput ((P +* I),(),k))) = (I ";" J) . (IC (Comput ((P +* I),(),k))) by
.= (P +* (I ";" J)) . (IC (Comput ((P +* I),(),k))) by
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(),k))) by
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) by ;
hence Comput ((P +* I),(),(k + 1)) = Comput ((P +* (I ";" J)),(),(k + 1)) by ; :: thesis: verum
end;
end;
A16: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A16, A4); :: thesis: verum