reconsider S = s as SCM+FSA-State ;
reconsider D = d as Element of SCM+FSA-Data-Loc by Def4;
S . D = s . d ;
hence s . d is Integer ; :: thesis: verum