set I = Load (<*> the Instructions of SCM+FSA );
take Load (<*> the Instructions of SCM+FSA ) ; :: thesis: Load (<*> the Instructions of SCM+FSA ) is pseudo-paraclosed

now

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

end;

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