let n, m be Nat; :: thesis: ( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds
n = len x ) & ( for x being FinSequence st x in dom f holds
m = len x ) implies n = m ) & ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m ) )

hereby :: thesis: ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m )

given x0 being FinSequence such that A2: x0 in dom f ; :: thesis: ( ( for x being FinSequence st x in dom f holds
n = len x ) & ( for x being FinSequence st x in dom f holds
m = len x ) implies n = m )
assume that
A3: for x being FinSequence st x in dom f holds
n = len x and
A4: for x being FinSequence st x in dom f holds
m = len x ; :: thesis: n = m
n = len x0 by A2, A3;
hence n = m by A2, A4; :: thesis: verum

end;

thus ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m ) ; :: thesis: verum