let B be Subset of (Bags 1); :: thesis: card B = card (BagN1 .: B)
reconsider F = BagN1 | B as Function ;
A1: rng F = BagN1 .: B by RELAT_1:115;
dom F = B by FUNCT_2:def 1;
hence card B = card (BagN1 .: B) by CARD_1:5, A1, WELLORD2:def 4; :: thesis: verum