defpred S₁[ Element of QC-WFF ] means F₂() . $1 = F₃() . $1;
A3: for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]

let k be Element of NAT ; :: thesis:
let P be QC-pred_symbol of k; :: thesis:
let l be QC-variable_list of k; :: thesis:
A4: P ! l is atomic by QC_LANG1:def 17;
hence F₂() . (P ! l) = F₅((P ! l)) by A1
.= F₃() . (P ! l) by A2, A4 ;
:: thesis:

end;

A5: for x being bound_QC-variable
for p being Element of QC-WFF st S₁[p] holds
S₁[ All x,p]

let x be bound_QC-variable; :: thesis:
let p be Element of QC-WFF ; :: thesis:
assume A6: F₂() . p = F₃() . p ; :: thesis:
A7: All x,p is universal by QC_LANG1:def 20;
then the_scope_of (All x,p) = p by QC_LANG1:def 27;
hence F₂() . (All x,p) = F₈((All x,p),(F₃() . (the_scope_of (All x,p)))) by A1, A6, A7
.= F₃() . (All x,p) by A2, A7 ;
:: thesis:

end;

A8: for p, q being Element of QC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q]

let p, q be Element of QC-WFF ; :: thesis:
assume A9: ( F₂() . p = F₃() . p & F₂() . q = F₃() . q ) ; :: thesis:
A10: p '&' q is conjunctive by QC_LANG1:def 19;
then A11: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 24, QC_LANG1:def 25;
hence F₂() . (p '&' q) = F₇((F₃() . p),(F₃() . q)) by A1, A9, A10
.= F₃() . (p '&' q) by A2, A10, A11 ;
:: thesis:

end;

A12: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p]

end;