let Al be QC-alphabet ; :: thesis: for B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ )
let B be Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]; :: thesis: for SQ being second_Q_comp of B st B is quantifiable holds
( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ )
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies ( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ ) )
assume B is quantifiable ; :: thesis: ( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ )
then Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ] by SUBSTUT1:def 24;
hence ( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ ) ; :: thesis: verum