let x be bound_QC-variable; :: thesis: ex i being Element of NAT st x. i = x
consider i, j being set such that
A1: i in {4} and
A2: j in NAT and
A3: [i,j] = x by ZFMISC_1:def 2;
reconsider j = j as Element of NAT by A2;
take j ; :: thesis: x. j = x
thus x. j = x by A1, A3, TARSKI:def 1; :: thesis: verum