index VERUM = 0 by Th21, QC_LANG3:24;
hence SepVar VERUM = ([:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM ) . [0 ,(id bound_QC-variables )] by Def6
.= VERUM by FUNCOP_1:13 ;
:: thesis: verum