let n1, n2 be Element of NAT ; :: thesis: ( ( for a being FinSequence st a in p holds
n1 = len a ) & ( for a being FinSequence st a in p holds
n2 = len a ) implies n1 = n2 )
assume that
A3: for a being FinSequence st a in p holds
n1 = len a and
A4: for a being FinSequence st a in p holds
n2 = len a ; :: thesis: n1 = n2
consider a being FinSequence such that
A5: a in p by A1;
len a = n1 by A3, A5;
hence n1 = n2 by A4, A5; :: thesis: verum