let A be QC-alphabet ; :: thesis: for a being free_QC-variable of A ex i being Element of NAT st A a. i = a
let a be free_QC-variable of A; :: thesis: ex i being Element of NAT st A a. i = a
consider x, y being set such that
A1: x in {6} and
A2: y in NAT and
A3: [x,y] = a by ZFMISC_1:def 2;
reconsider i = y as Element of NAT by A2;
take i ; :: thesis: A a. i = a
thus A a. i = a by A1, A3, TARSKI:def 1; :: thesis: verum