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