per cases ( dom B is infinite or dom B is finite ) ;
suppose dom B is infinite ; :: thesis: p ^ B is with_cardinal_domain
then ( omega c= dom B & dom p in omega ) by ORDINAL1:16, CARD_1:61;
hence p ^ B is with_cardinal_domain by Th56; :: thesis: verum
end;
suppose dom B is finite ; :: thesis: p ^ B is with_cardinal_domain
then B is XFinSequence ;
hence p ^ B is with_cardinal_domain ; :: thesis: verum
end;
end;