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:63; :: thesis: verum