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]

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of k holds S₁[P ! l]
let l be QC-variable_list of k; :: thesis: S₁[P ! l]
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: verum

end;

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

proof

let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st S₁[p] holds
S₁[ All (x,p)]
let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume A6: F₂() . p = F₃() . p ; :: thesis: S₁[ All (x,p)]
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: verum

end;

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

proof

let p, q be Element of QC-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A9: ( F₂() . p = F₃() . p & F₂() . q = F₃() . q ) ; :: thesis: S₁[p '&' q]
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: verum

end;

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

proof

let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A13: F₂() . p = F₃() . p ; :: thesis: S₁[ 'not' p]
A14: 'not' p is negative by QC_LANG1:def 18;
then A15: the_argument_of ('not' p) = p by QC_LANG1:def 23;
hence F₂() . ('not' p) = F₆((F₃() . p)) by A1, A13, A14
.= F₃() . ('not' p) by A2, A14, A15 ;
:: thesis: verum

end;

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