let p, q be FinSequence of the Instructions of SCM+FSA ; :: thesis: ( p c= q implies Load p c= Load q )
assume p c= q ; :: thesis: Load p c= Load q
then ex p9 being FinSequence of the Instructions of SCM+FSA st p ^ p9 = q by FINSEQ_4:97;
hence Load p c= Load q by Th31; :: thesis: verum