Proof of bsublist_functionality_wrt_bsublist