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 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 object ; :: 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 Nat ;
q . i in Funcs ((p . i),(p . (i + 1))) by A1, A2;
hence q . i is set ; :: thesis: verum