reconsider D = d as Element of SCM+FSA-Data*-Loc by Def3;
reconsider S = s as SCM+FSA-State by CARD_3:107;
S . D = s . d ;
hence s . d is FinSequence of INT ; :: thesis: verum