set Q = P +~ (halt SCM+FSA ),(goto l);
set PP = ((halt SCM+FSA ) .--> (goto l)) * P;
A1: dom (P +~ (halt SCM+FSA ),(goto l)) = dom P by FUNCT_4:105;
A2: for x being set st x in dom (P +~ (halt SCM+FSA ),(goto l)) holds
(P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x

proof

let x be set ; :: thesis: ( x in dom (P +~ (halt SCM+FSA ),(goto l)) implies (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x )
assume A3: x in dom (P +~ (halt SCM+FSA ),(goto l)) ; :: thesis: (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x

per cases ( x in dom (((halt SCM+FSA ) .--> (goto l)) * P) or not x in dom (((halt SCM+FSA ) .--> (goto l)) * P) ) ;

suppose A4: x in dom (((halt SCM+FSA ) .--> (goto l)) * P) ; :: thesis: (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x

then P . x in dom ((halt SCM+FSA ) .--> (goto l)) by FUNCT_1:21;
then A5: P . x = halt SCM+FSA by FUNCOP_1:90;
(((halt SCM+FSA ) .--> (goto l)) * P) . x = ((halt SCM+FSA ) .--> (goto l)) . (P . x) by A4, FUNCT_1:22;
then A6: (((halt SCM+FSA ) .--> (goto l)) * P) . x = goto l by A5, FUNCOP_1:87;
A7: (P +~ (halt SCM+FSA ),(goto l)) . x = (((halt SCM+FSA ) .--> (goto l)) * P) . x by A4, FUNCT_4:14;
dom P c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A1, A3;
the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by AMI_1:def 14;
hence (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x by A7, A6; :: thesis: verum

end;

suppose A8: not x in dom (((halt SCM+FSA ) .--> (goto l)) * P) ; :: thesis: (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x

dom (P +~ (halt SCM+FSA ),(goto l)) = (dom P) \/ (dom (((halt SCM+FSA ) .--> (goto l)) * P)) by FUNCT_4:def 1;
then A9: x in dom P by A3, A8, XBOOLE_0:def 3;
(P +~ (halt SCM+FSA ),(goto l)) . x = P . x by A8, FUNCT_4:12;
hence (P +~ (halt SCM+FSA ),(goto l)) . x in the Object-Kind of SCM+FSA . x by A9, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

reconsider Q = P +~ (halt SCM+FSA ),(goto l) as FinPartState of SCM+FSA by A2, FUNCT_1:def 20;
dom Q c= NAT by RELAT_1:def 18;
hence P +~ (halt SCM+FSA ),(goto l) is preProgram of SCM+FSA ; :: thesis: verum