let l1, l2 be Nat; :: thesis: ( ex p being FinSequence of NAT st
( p in T & len p = l1 ) & ( for p being FinSequence of NAT st p in T holds
len p <= l1 ) & ex p being FinSequence of NAT st
( p in T & len p = l2 ) & ( for p being FinSequence of NAT st p in T holds
len p <= l2 ) implies l1 = l2 )
given p1 being FinSequence of NAT such that A17: ( p1 in T & len p1 = l1 ) ; :: thesis: ( ex p being FinSequence of NAT st
( p in T & not len p <= l1 ) or for p being FinSequence of NAT holds
( not p in T or not len p = l2 ) or ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
assume A18: for p being FinSequence of NAT st p in T holds
len p <= l1 ; :: thesis: ( for p being FinSequence of NAT holds
( not p in T or not len p = l2 ) or ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
given p2 being FinSequence of NAT such that A19: ( p2 in T & len p2 = l2 ) ; :: thesis: ( ex p being FinSequence of NAT st
( p in T & not len p <= l2 ) or l1 = l2 )
assume for p being FinSequence of NAT st p in T holds
len p <= l2 ; :: thesis: l1 = l2
then A20: l1 <= l2 by A17;
l2 <= l1 by A18, A19;
hence l1 = l2 by A20, XXREAL_0:1; :: thesis: verum