now

A1: IC SCM+FSA in dom ((f := p) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
let s be State of SCM+FSA; :: thesis: ( (f := p) +* (Start-At (0,SCM+FSA)) c= s implies ProgramPart s halts_on s )
assume A2: (f := p) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: ProgramPart s halts_on s
IC s = IC ((f := p) +* (Start-At (0,SCM+FSA))) by A2, A1, GRFUNC_1:8
.= 0 by COMPOS_1:142 ;
then s is 0 -started by COMPOS_1:def 20;
hence ProgramPart s halts_on s by A2, Lm7, COMPOS_1:131; :: thesis: verum

end;

then (f := p) +* (Start-At (0,SCM+FSA)) is halting by EXTPRO_1:def 10;
hence f := p is parahalting by SCMFSA6B:def 3; :: thesis: verum