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 Element of 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 Element of NAT st i in dom p holds
p . i in Funcs (q . i),(q . (i + 1)) ) ) by Def10; :: thesis: verum

end;

let x be set ; :: according to FUNCT_1:def 15 :: 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 Element of NAT ;
len q = (len p) + 1 by Def10;
then ( i in dom q & i + 1 in dom q ) by A1, Th24;
then reconsider X = q . i, Y = q . (i + 1) as non empty set ;
p . i in Funcs X,Y by A1, Def10;
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