let i be Integer; :: thesis: for d being Data-Location holds i in (the_Values_of SCM) . d
let d be Data-Location; :: thesis: i in (the_Values_of SCM) . d
d in SCM-Data-Loc by AMI_2:def 16;
then (SCM-VAL * SCM-OK) . d = INT by AMI_2:8;
hence i in (the_Values_of SCM) . d by INT_1:def 2; :: thesis: verum