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;