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 A1: p . y in rng p by FUNCT_1:def 3;
rng p c= x by FINSEQ_1:def 4;
hence p . y in x by A1; :: thesis: verum