let A be QC-alphabet ; :: thesis: for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
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 B1, B2 be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; :: 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, XTUPLE_0:1;
then A5: ( B1 `2 = B2 `2 & (B1 `1) `1 = (B2 `1) `1 ) by QC_LANG2:5;
ex a, b being object st
( a in QC-Sub-WFF A & b in bound_QC-variables A & B2 = [a,b] ) by ZFMISC_1:def 2;
then A6: B2 = [(B2 `1),(B2 `2)] ;
ex a, b being object st
( a in QC-Sub-WFF A & b in bound_QC-variables A & B1 = [a,b] ) by ZFMISC_1:def 2;
then A7: B1 = [(B1 `1),(B1 `2)] ;
A8: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10;
(B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A1, Def23;
hence B1 = B2 by A2, A3, A4, A5, A8, A7, A6, Def23; :: thesis: verum