JumpPart (halt SCM+FSA) is empty by Lm3, RECDEF_2:def 2;
then halt SCM+FSA is ins-loc-free by COMPOS_1:def 37;
hence SCM+FSA is proper-halt by COMPOS_1:def 39; :: thesis: ( SCM+FSA is realistic & SCM+FSA is IC-Ins-separated & SCM+FSA is definite )
thus SCM+FSA is realistic :: thesis: ( SCM+FSA is IC-Ins-separated & SCM+FSA is definite )

proof

assume the ZeroF of SCM+FSA in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
hence contradiction by FUNCT_7:def 1, SCMFSA_1:5; :: thesis: verum

end;

ObjectKind (IC ) = NAT by FUNCT_7:def 1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by COMPOS_1:def 6; :: thesis: SCM+FSA is definite
let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA
thus the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by SCMFSA_1:11; :: thesis: verum