deffunc H1( Element of QC-WFF F1(), Element of F2()) -> Element of F2() = F7((bound_in $1),$2);
deffunc H2( Element of QC-WFF F1()) -> Element of F2() = F4((the_arity_of (the_pred_symbol_of $1)),(the_pred_symbol_of $1),(the_arguments_of $1));
consider F being Function of (QC-WFF F1()),F2() such that
A1: ( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = H2(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = H1(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch 3();
 reconsider G = F | (CQC-WFF F1()) as Function of (CQC-WFF F1()),F2() by FUNCT_2:32;
take G ; :: thesis: ( G . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) ) ) )
thus G . (VERUM F1()) = F3() by A1, FUNCT_1:49; :: thesis: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let r, s be Element of CQC-WFF F1(); :: thesis: for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let x be bound_QC-variable of F1(); :: thesis: for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let k be Element of NAT ; :: thesis: for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let l be CQC-variable_list of k,F1(); :: thesis: for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let P be QC-pred_symbol of k,F1(); :: thesis: ( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
A2: the_arity_of P = k by QC_LANG1:11;
A3: P ! l is atomic by QC_LANG1:def 18;
then A4: ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P ) by QC_LANG1:def 22, QC_LANG1:def 23;
thus G . (P ! l) = F . (P ! l) by FUNCT_1:49
.= F4(k,P,l) by A1, A3, A4, A2 ; :: thesis: ( G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
set r9 = G . r;
set s9 = G . s;
A5: G . r = F . r by FUNCT_1:49;
A6: r '&' s is conjunctive by QC_LANG1:def 20;
then A7: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s ) by QC_LANG1:def 25, QC_LANG1:def 26;
A8: 'not' r is negative by QC_LANG1:def 19;
then A9: the_argument_of ('not' r) = r by QC_LANG1:def 24;
thus G . ('not' r) = F . ('not' r) by FUNCT_1:49
.= F5((G . r)) by A1, A5, A8, A9 ; :: thesis: ( G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
A10: G . s = F . s by FUNCT_1:49;
thus G . (r '&' s) = F . (r '&' s) by FUNCT_1:49
.= F6((G . r),(G . s)) by A1, A5, A10, A6, A7 ; :: thesis: G . (All (x,r)) = F7(x,(G . r))
A11: All (x,r) is universal by QC_LANG1:def 21;
then A12: ( bound_in (All (x,r)) = x & the_scope_of (All (x,r)) = r ) by QC_LANG1:def 27, QC_LANG1:def 28;
thus G . (All (x,r)) = F . (All (x,r)) by FUNCT_1:49
.= F7(x,(G . r)) by A1, A5, A11, A12 ; :: thesis: verum