consider F being Function of QC-WFF ,F₁() such that
A3: F₇(F₈()) = F . F₈() and
A4: 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;
let d1, d2 be Element of F₁(); :: thesis: ( d1 = F₇((the_left_argument_of F₈())) & d2 = F₇((the_right_argument_of F₈())) implies F₇(F₈()) = F₅(d1,d2) )
assume ( d1 = F₇((the_left_argument_of F₈())) & d2 = F₇((the_right_argument_of F₈())) ) ; :: thesis: F₇(F₈()) = F₅(d1,d2)
then ( F . (the_left_argument_of F₈()) = d1 & F . (the_right_argument_of F₈()) = d2 ) by A1, A4;
hence F₇(F₈()) = F₅(d1,d2) by A2, A3, A4; :: thesis: verum