now

A1: IC SCM+FSA in dom ((f := p) +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
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 = s . (IC SCM+FSA ) by COMPOS_1:def 9
.= ((f := p) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A2, A1, GRFUNC_1:8
.= 0 by SF_MASTR:66 ;
hence ProgramPart s halts_on s by A2, Lm7, SCMFSA6B:5; :: thesis: verum

end;

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