let x, y be set ; :: thesis: for p being FinSequence of x st y in dom p holds
p . y in x
let p be FinSequence of x; :: thesis: ( y in dom p implies p . y in x )
assume y in dom p ; :: thesis: p . y in x
then ( p . y in rng p & rng p c= x ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence p . y in x ; :: thesis: verum