consider c being FinSequence of D such that
A2: c in p by A1, Def9;
for a being FinSequence of D st a in p holds
len c = len a by A2, Def7;
hence ex b₁ being Element of NAT st
for a being FinSequence of D st a in p holds
b₁ = len a ; :: thesis: verum