set q = (intloc n) .--> i;
i in INT by INT_1:def 2;
then A2: ( rng ((intloc n) .--> i) = {i} & {i} c= INT ) by FUNCOP_1:8, ZFMISC_1:31;
let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in dom ((intloc n) .--> i) or ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x )
assume A3: x in dom ((intloc n) .--> i) ; :: thesis: ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x
reconsider l = x as Int-Location by A3, TARSKI:def 1;
A4: (the_Values_of SCM+FSA) . l = Values l
.= INT by SCMFSA_2:11 ;
((intloc n) .--> i) . x in rng ((intloc n) .--> i) by A3, FUNCT_1:def 3;
hence ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x by A4, A2; :: thesis: verum