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