let Al be QC-alphabet ; for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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 B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]; for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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; for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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 Al),(bound_QC-variables Al):]; 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; ( B is quantifiable & B1 is quantifiable & Sub_All (B,SQ) = Sub_All (B1,SQ1) implies ( B `2 = B1 `2 & SQ = SQ1 ) )
assume that
A1:
B is quantifiable
and
A2:
( B1 is quantifiable & Sub_All (B,SQ) = Sub_All (B1,SQ1) )
; ( B `2 = B1 `2 & SQ = SQ1 )
Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ]
by A1, SUBSTUT1:def 24;
then A3:
[(All ((B `2),((B `1) `1))),SQ] = [(All ((B1 `2),((B1 `1) `1))),SQ1]
by A2, SUBSTUT1:def 24;
then
All ((B `2),((B `1) `1)) = All ((B1 `2),((B1 `1) `1))
by XTUPLE_0:1;
hence
( B `2 = B1 `2 & SQ = SQ1 )
by A3, QC_LANG2:5, XTUPLE_0:1; verum