let p be FinSequence; :: thesis: ( p is empty implies p is FuncSeq-like )
assume A1: p is empty ; :: thesis: p is FuncSeq-like
take q = <*{}*>; :: according to FUNCT_7:def 8 :: thesis: ( len q = (len p) + 1 & ( for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1))) ) )
thus len q = (len p) + 1 by A1, FINSEQ_1:40; :: thesis: for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1)))
thus for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1))) by A1; :: thesis: verum