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 p' being FinSequence of the Instructions of SCM+FSA st p ^ p' = q by FINSEQ_4:97;
hence Load p c= Load q by Th31; :: thesis: verum