consider F being Function of (QC-WFF F1()),F2() such that
A3:
F8(F9()) = F . F9()
and
A4:
for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F5(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F6(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F7(p,d1) ) )
by A1;
let d1, d2 be Element of F2(); ( d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) implies F8(F9()) = F6(d1,d2) )
assume
( d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) )
; F8(F9()) = F6(d1,d2)
then
( F . (the_left_argument_of F9()) = d1 & F . (the_right_argument_of F9()) = d2 )
by A1, A4;
hence
F8(F9()) = F6(d1,d2)
by A2, A3, A4; verum