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

let k be Nat; :: thesis:
let P be QC-pred_symbol of k,F₁(); :: thesis:
let l be QC-variable_list of k,F₁(); :: thesis:
A4: P ! l is atomic ;
hence F₃() . (P ! l) = F₆((P ! l)) by A1
.= F₄() . (P ! l) by A2, A4 ;
:: thesis:

end;

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

let x be bound_QC-variable of F₁(); :: thesis:
let p be Element of QC-WFF F₁(); :: thesis:
assume A6: F₃() . p = F₄() . p ; :: thesis:
A7: All (x,p) is universal ;
then the_scope_of (All (x,p)) = p by QC_LANG1:def 28;
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 F₁() st S₁[p] & S₁[q] holds
S₁[p '&' q]

let p, q be Element of QC-WFF F₁(); :: thesis:
assume A9: ( F₃() . p = F₄() . p & F₃() . q = F₄() . q ) ; :: thesis:
A10: p '&' q is conjunctive ;
then A11: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 25, QC_LANG1:def 26;
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 F₁() st S₁[p] holds
S₁[ 'not' p]

let p be Element of QC-WFF F₁(); :: thesis:
assume A13: F₃() . p = F₄() . p ; :: thesis:
A14: 'not' p is negative ;
then A15: the_argument_of ('not' p) = p by QC_LANG1:def 24;
hence F₃() . ('not' p) = F₇((F₄() . p)) by A1, A13, A14
.= F₄() . ('not' p) by A2, A14, A15 ;
:: thesis:

end;

F₃() . (VERUM F₁()) = F₅() by A1;
then A16: S₁[ VERUM F₁()] by A2;
for p being Element of QC-WFF F₁() holds S₁[p] from QC_LANG1:sch 1(A3, A16, A12, A8, A5);
hence F₃() = F₄() by FUNCT_2:63; :: thesis: