consider F being Function of QC-WFF ,F₁() such that
A2: ( F₂(VERUM ) = F . VERUM & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM implies F . p = F₃() ) & ( p is atomic implies F . p = F₄(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₅(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₆(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₇(p,d1) ) ) ) ) by A1;
thus F₂(VERUM ) = F₃() by A2; :: thesis: verum