let B be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]; :: thesis: for SQ being second_Q_comp of B
for B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 holds
( B `2 = B1 `2 & SQ = SQ1 )
let SQ be second_Q_comp of B; :: thesis: for B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 holds
( B `2 = B1 `2 & SQ = SQ1 )
let B1 be Element of [:QC-Sub-WFF ,bound_QC-variables :]; :: thesis: for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 holds
( B `2 = B1 `2 & SQ = SQ1 )
let SQ1 be second_Q_comp of B1; :: thesis: ( B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 implies ( B `2 = B1 `2 & SQ = SQ1 ) )
assume A1: ( B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 ) ; :: thesis: ( B `2 = B1 `2 & SQ = SQ1 )
then Sub_All B,SQ = [(All (B `2 ),((B `1 ) `1 )),SQ] by SUBSTUT1:def 24;
then [(All (B `2 ),((B `1 ) `1 )),SQ] = [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] by A1, SUBSTUT1:def 24;
then ( All (B `2 ),((B `1 ) `1 ) = All (B1 `2 ),((B1 `1 ) `1 ) & SQ = SQ1 ) by ZFMISC_1:33;
hence ( B `2 = B1 `2 & SQ = SQ1 ) by QC_LANG2:6; :: thesis: verum