let b be bag of 1; :: thesis: ( dom b = {0} & rng b = {(b . 0)} )
dom b = {0} by CARD_1:49, PARTFUN1:def 2;
hence ( dom b = {0} & rng b = {(b . 0)} ) by FUNCT_1:4; :: thesis: verum