let B1, B2 be Element of [:QC-Sub-WFF ,bound_QC-variables :]; :: thesis: for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All B1,SQ1 = Sub_All B2,SQ2 holds
B1 = B2
let SQ1 be second_Q_comp of B1; :: thesis: for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All B1,SQ1 = Sub_All B2,SQ2 holds
B1 = B2
let SQ2 be second_Q_comp of B2; :: thesis: ( B1 is quantifiable & B2 is quantifiable & Sub_All B1,SQ1 = Sub_All B2,SQ2 implies B1 = B2 )
assume that
A1: B1 is quantifiable and
A2: B2 is quantifiable and
A3: Sub_All B1,SQ1 = Sub_All B2,SQ2 ; :: thesis: B1 = B2
A4: ( Sub_All B1,SQ1 = [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] & Sub_All B2,SQ2 = [(All (B2 `2 ),((B2 `1 ) `1 )),SQ2] ) by A1, A2, Def24;
then All (B1 `2 ),((B1 `1 ) `1 ) = All (B2 `2 ),((B2 `1 ) `1 ) by A3, ZFMISC_1:33;
then A5: ( B1 `2 = B2 `2 & (B1 `1 ) `1 = (B2 `1 ) `1 ) by QC_LANG2:6;
ex a, b being set st
( a in QC-Sub-WFF & b in bound_QC-variables & B2 = [a,b] ) by ZFMISC_1:def 2;
then A6: B2 = [(B2 `1 ),(B2 `2 )] by MCART_1:8;
ex a, b being set st
( a in QC-Sub-WFF & b in bound_QC-variables & B1 = [a,b] ) by ZFMISC_1:def 2;
then A7: B1 = [(B1 `1 ),(B1 `2 )] by MCART_1:8;
A8: ( B1 `1 = [((B1 `1 ) `1 ),((B1 `1 ) `2 )] & B2 `1 = [((B2 `1 ) `1 ),((B2 `1 ) `2 )] ) by Th10;
(B1 `1 ) `2 = QSub . [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] by A1, Def23;
hence B1 = B2 by A2, A3, A4, A5, A8, A7, A6, Def23; :: thesis: verum