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

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of
for e being Element of vSUB holds S₁[ Sub_P P,l,e]
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of
for e being Element of vSUB holds S₁[ Sub_P P,l,e]
let l be QC-variable_list of ; :: thesis: for e being Element of vSUB holds S₁[ Sub_P P,l,e]
let e be Element of vSUB ; :: 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 S being Element of QC-Sub-WFF st S is Sub_VERUM holds
S₁[S]

proof

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

end;

A5: for S being Element of QC-Sub-WFF st S₁[S] holds
S₁[ Sub_not S]

proof

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

end;

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

proof

let S1, S2 be Element of QC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 & S₁[S1] & S₁[S2] implies S₁[ Sub_& S1,S2] )
assume A9: ( S1 `2 = S2 `2 & F₂() . S1 = F₃() . S1 & F₂() . S2 = F₃() . S2 ) ; :: thesis: S₁[ Sub_& S1,S2]
A10: Sub_& S1,S2 is Sub_conjunctive by A9, Th13;
A11: ( Sub_the_left_argument_of (Sub_& S1,S2) = S1 & Sub_the_right_argument_of (Sub_& S1,S2) = S2 ) by A9, Th18, Th19;
hence F₂() . (Sub_& S1,S2) = F₇((F₃() . S1),(F₃() . S2)) by A1, A9, A10
.= F₃() . (Sub_& S1,S2) by A2, A10, A11 ;
:: thesis: verum

end;

A12: for x being bound_QC-variable
for S being Element of QC-Sub-WFF
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; :: thesis: for S being Element of QC-Sub-WFF
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 ; :: 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 A13: ( [S,x] is quantifiable & F₂() . S = F₃() . S ) ; :: thesis: S₁[ Sub_All [S,x],SQ]
A14: Sub_All [S,x],SQ is Sub_universal by A13, Th14;
Sub_the_scope_of (Sub_All [S,x],SQ) = [S,x] `1 by A13, Th21;
then Sub_the_scope_of (Sub_All [S,x],SQ) = S by MCART_1:7;
hence F₂() . (Sub_All [S,x],SQ) = F₈((Sub_All [S,x],SQ),(F₃() . (Sub_the_scope_of (Sub_All [S,x],SQ)))) by A1, A13, A14
.= F₃() . (Sub_All [S,x],SQ) by A2, A14 ;
:: thesis: verum

end;

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