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