set q = (intloc n) .--> i;
A1: dom ((intloc n) .--> i) = {(intloc n)} by FUNCOP_1:13;
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 set ; :: according to FUNCT_1:def 14 :: thesis: ( not x in proj1 ((intloc n) .--> i) or ((intloc n) .--> i) . x in the Object-Kind of SCM+FSA . x )
assume A3: x in dom ((intloc n) .--> i) ; :: thesis: ((intloc n) .--> i) . x in the Object-Kind of SCM+FSA . x
intloc n in Int-Locations by SCMFSA_2:2;
then dom ((intloc n) .--> i) c= Int-Locations by A1, ZFMISC_1:31;
then reconsider l = x as Int-Location by A3, SCMFSA_2:4;
A4: the Object-Kind of SCM+FSA . l = ObjectKind 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 Object-Kind of SCM+FSA . x by A4, A2; :: thesis: verum