let Al be QC-alphabet ; :: thesis: 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 & CQCSub_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):]; :: thesis: 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 & CQCSub_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 Al),(bound_QC-variables Al):]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & CQCSub_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):]; :: thesis: for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & CQCSub_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 & CQCSub_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 and
A3: CQCSub_All (B,SQ) = Sub_All (B1,SQ1) ; :: thesis: ( B `2 = B1 `2 & SQ = SQ1 )
Sub_All (B,SQ) = Sub_All (B1,SQ1) by A1, A3, Def5;
hence ( B `2 = B1 `2 & SQ = SQ1 ) by A1, A2, Th35; :: thesis: verum