let i be Nat; :: thesis: for Y being set holds i -tuples_on Y = Funcs ((Seg i),Y)
let Y be set ; :: thesis: i -tuples_on Y = Funcs ((Seg i),Y)

per cases ( Y is empty or not Y is empty ) ;

suppose A1: Y is empty ; :: thesis: i -tuples_on Y = Funcs ((Seg i),Y)

per cases ( i is zero or not i is zero ) ;

suppose i is zero ; :: thesis: i -tuples_on Y = Funcs ((Seg i),Y)

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: verum

end;

suppose not i is zero ; :: thesis: i -tuples_on Y = Funcs ((Seg i),Y)

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

end;

end;

end;

suppose not Y is empty ; :: thesis: i -tuples_on Y = Funcs ((Seg i),Y)

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

end;

end;