set I = Load (<*> the Instructions of SCM+FSA );

A1: now

let s be State of SCM+FSA ; :: thesis: Load (<*> the Instructions of SCM+FSA ) is_pseudo-closed_on s
A2: card (Load (<*> the Instructions of SCM+FSA )) = 0 by CARD_1:47, SCMFSA_7:25;
A3: IC SCM+FSA in dom ((Load (<*> the Instructions of SCM+FSA )) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A4: IC (Computation (s +* ((Load (<*> the Instructions of SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = (s +* ((Load (<*> the Instructions of SCM+FSA )) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:13
.= ((Load (<*> the Instructions of SCM+FSA )) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= insloc (card (Load (<*> the Instructions of SCM+FSA ))) by A2, SF_MASTR:66
.= insloc (card (ProgramPart (Load (<*> the Instructions of SCM+FSA )))) by AMI_1:105 ;
for n being Element of NAT st n < 0 holds
IC (Computation (s +* ((Load (<*> the Instructions of SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (Load (<*> the Instructions of SCM+FSA )) by NAT_1:2;
hence Load (<*> the Instructions of SCM+FSA ) is_pseudo-closed_on s by A4, Def3; :: thesis: verum

end;

take Load (<*> the Instructions of SCM+FSA ) ; :: thesis: Load (<*> the Instructions of SCM+FSA ) is pseudo-paraclosed
thus Load (<*> the Instructions of SCM+FSA ) is pseudo-paraclosed by A1, Def4; :: thesis: verum