let q be FinSequence; :: thesis: ( q is FuncSeq-like implies q is Function-yielding )
given p being FinSequence such that len p = (len q) + 1 and
A1: for i being Element of NAT st i in dom q holds
q . i in Funcs (p . i),(p . (i + 1)) ; :: according to FUNCT_7:def 8 :: thesis: q is Function-yielding
let i be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in proj1 q or q . i is set )
assume A2: i in dom q ; :: thesis: q . i is set
then reconsider i = i as Element of NAT ;
q . i in Funcs (p . i),(p . (i + 1)) by A1, A2;
then ex f being Function st
( q . i = f & dom f = p . i & rng f c= p . (i + 1) ) by FUNCT_2:def 2;
hence q . i is set ; :: thesis: verum