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 k
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 k
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 k
for e being Element of vSUB holds S₁[ Sub_P P,l,e]
let l be QC-variable_list of k; :: 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 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 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, Th14;
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 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, A6, A7
.= F₃() . (Sub_All [S,x],SQ) by A2, A7 ;
:: thesis: verum

end;

A8: 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 A9: S is 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 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 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, Th13, 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 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 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 holds S₁[S] from SUBSTUT1:sch 1(A3, A8, A15, A10, A4);
hence F₂() = F₃() by FUNCT_2:113; :: thesis: verum