let A be QC-alphabet ; :: thesis: SepVar (VERUM A) = VERUM A
index (VERUM A) = 0 A by Th22;
hence SepVar (VERUM A) = ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A)) . [(0 A),(id (bound_QC-variables A))] by Def7
.= VERUM A ;
:: thesis: verum