reconsider pp = p as FinSequence of D by FOMODEL0:26;
len (h * pp) = len pp by FINSEQ_2:33;
hence for b₁ being FinSequence st b₁ = h * p holds
b₁ is len p -element by CARD_1:def 7; :: thesis: verum