consider F being Function of (QC-WFF F₁()),F₂() such that
A3: F₈(F₉()) = F . F₉() and
A4: for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() 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