theorem :: SUBSTUT2:13

for Al being QC-alphabet
for x, y being bound_QC-variable of Al holds (VERUM Al) . (x,y) = VERUM Al