let n, k be Nat; :: thesis: for f being FinSequence st f in doms (n,k) holds
len f = k
let f be FinSequence; :: thesis: ( f in doms (n,k) implies len f = k )
assume f in doms (n,k) ; :: thesis: len f = k
then ex s being Element of (Seg n) * st
( f = s & len s = k ) ;
hence len f = k ; :: thesis: verum