let i be Nat; :: thesis:
let Y be set ; :: thesis:

suppose A1: Y is empty ; :: thesis:

suppose i is zero ; :: thesis:

then ( i is zero & Seg i = {} ) ;
then ( Funcs ((Seg i),Y) = {{}} & i -tuples_on Y = {{}} ) by FUNCT_5:57, Lm6;
hence i -tuples_on Y = Funcs ((Seg i),Y) ; :: thesis:

end;

suppose not i is zero ; :: thesis:

then ( Funcs ((Seg i),Y) = {} & i -tuples_on Y = {} ) by FINSEQ_3:119, A1;
hence i -tuples_on Y = Funcs ((Seg i),Y) ; :: thesis:

end;

end;

end;

suppose not Y is empty ; :: thesis:

then reconsider YY = Y as non empty set ;
thus i -tuples_on Y = Funcs ((Seg i),Y) by FINSEQ_2:93; :: thesis:

end;

end;