let A be QC-alphabet ; for a being Element of free_QC-variables A
for x being Element of bound_QC-variables A holds a <> x
let a be Element of free_QC-variables A; for x being Element of bound_QC-variables A holds a <> x
let x be Element of bound_QC-variables A; a <> x
consider x1, x2 being object such that
A1:
x1 in {4}
and
x2 in QC-symbols A
and
A2:
x = [x1,x2]
by ZFMISC_1:def 2;
consider a1, a2 being object such that
A3:
a1 in {6}
and
a2 in NAT
and
A4:
a = [a1,a2]
by ZFMISC_1:def 2;
A5:
a1 = 6
by A3, TARSKI:def 1;
x1 = 4
by A1, TARSKI:def 1;
hence
a <> x
by A2, A4, A5, XTUPLE_0:1; verum