let p be FuncSequence of q; :: thesis: ( p is FuncSeq-like & p is non-empty )
thus p is FuncSeq-like :: thesis: p is non-empty

proof

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 & ( for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1))) ) ) by Def9; :: thesis: verum

end;

let x be object ; :: according to FUNCT_1:def 9 :: thesis: ( not x in proj1 p or not p . x is empty )
assume A1: x in dom p ; :: thesis: not p . x is empty
then reconsider i = x as Nat ;
len q = (len p) + 1 by Def9;
then ( i in dom q & i + 1 in dom q ) by A1, Th22;
then reconsider X = q . i, Y = q . (i + 1) as non empty set ;
p . i in Funcs (X,Y) by A1, Def9;
then ex f being Function st
( p . x = f & dom f = X & rng f c= Y ) by FUNCT_2:def 2;
hence not p . x is empty ; :: thesis: verum