defpred S₁[ Element of QC-Sub-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₁()
for e being Element of vSUB F₁() holds S₁[ Sub_P (P,l,e)]

proof

let k be Nat; :: thesis: for P being QC-pred_symbol of k,F₁()
for l being QC-variable_list of k,F₁()
for e being Element of vSUB F₁() holds S₁[ Sub_P (P,l,e)]
let P be QC-pred_symbol of k,F₁(); :: thesis: for l being QC-variable_list of k,F₁()
for e being Element of vSUB F₁() holds S₁[ Sub_P (P,l,e)]
let l be QC-variable_list of k,F₁(); :: thesis: for e being Element of vSUB F₁() holds S₁[ Sub_P (P,l,e)]
let e be Element of vSUB F₁(); :: thesis: S₁[ Sub_P (P,l,e)]
thus F₃() . (Sub_P (P,l,e)) = F₆((Sub_P (P,l,e))) by A1
.= F₄() . (Sub_P (P,l,e)) by A2 ; :: thesis: verum

end;

A4: for x being bound_QC-variable of F₁()
for S being Element of QC-Sub-WFF F₁()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S₁[S] holds
S₁[ Sub_All ([S,x],SQ)]

proof

let x be bound_QC-variable of F₁(); :: thesis: for S being Element of QC-Sub-WFF F₁()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S₁[S] holds
S₁[ Sub_All ([S,x],SQ)]
let S be Element of QC-Sub-WFF F₁(); :: thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S₁[S] holds
S₁[ Sub_All ([S,x],SQ)]
let SQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & S₁[S] implies S₁[ Sub_All ([S,x],SQ)] )
assume that
A5: [S,x] is quantifiable and
A6: F₃() . S = F₄() . S ; :: thesis: S₁[ Sub_All ([S,x],SQ)]
A7: Sub_All ([S,x],SQ) is Sub_universal by A5;
Sub_the_scope_of (Sub_All ([S,x],SQ)) = [S,x] `1 by A5, Th21;
then Sub_the_scope_of (Sub_All ([S,x],SQ)) = S ;
hence F₃() . (Sub_All ([S,x],SQ)) = F₉(F₁(),(Sub_All ([S,x],SQ)),(F₄() . (Sub_the_scope_of (Sub_All ([S,x],SQ))))) by A1, A6, A7
.= F₄() . (Sub_All ([S,x],SQ)) by A2, A7 ;
:: thesis: verum

end;

A8: for S being Element of QC-Sub-WFF F₁() st S is F₁() -Sub_VERUM holds
S₁[S]

proof

let S be Element of QC-Sub-WFF F₁(); :: thesis: ( S is F₁() -Sub_VERUM implies S₁[S] )
assume A9: S is F₁() -Sub_VERUM ; :: thesis: S₁[S]
then F₃() . S = F₅() by A1;
hence S₁[S] by A2, A9; :: thesis: verum

end;

A10: for S1, S2 being Element of QC-Sub-WFF F₁() st S1 `2 = S2 `2 & S₁[S1] & S₁[S2] holds
S₁[ Sub_& (S1,S2)]

proof

let S1, S2 be Element of QC-Sub-WFF F₁(); :: thesis: ( S1 `2 = S2 `2 & S₁[S1] & S₁[S2] implies S₁[ Sub_& (S1,S2)] )
assume that
A11: S1 `2 = S2 `2 and
A12: ( F₃() . S1 = F₄() . S1 & F₃() . S2 = F₄() . S2 ) ; :: thesis: S₁[ Sub_& (S1,S2)]
A13: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A11, Th19;
A14: ( Sub_& (S1,S2) is Sub_conjunctive & Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 ) by A11, Th18;
hence F₃() . (Sub_& (S1,S2)) = F₈((F₄() . S1),(F₄() . S2)) by A1, A12, A13
.= F₄() . (Sub_& (S1,S2)) by A2, A14, A13 ;
:: thesis: verum

end;

A15: for S being Element of QC-Sub-WFF F₁() st S₁[S] holds
S₁[ Sub_not S]

proof

let S be Element of QC-Sub-WFF F₁(); :: thesis: ( S₁[S] implies S₁[ Sub_not S] )
assume A16: F₃() . S = F₄() . S ; :: thesis: S₁[ Sub_not S]
A17: Sub_the_argument_of (Sub_not S) = S by Def30;
hence F₃() . (Sub_not S) = F₇((F₄() . S)) by A1, A16
.= F₄() . (Sub_not S) by A2, A17 ;
:: thesis: verum

end;

for S being Element of QC-Sub-WFF F₁() holds S₁[S] from SUBSTUT1:sch 1(A3, A8, A15, A10, A4);
hence F₃() = F₄() by FUNCT_2:63; :: thesis: verum