let X, Y be set ; :: thesis: for f being homogeneous PartFunc of (X *),Y holds dom f c= (arity f) -tuples_on X
let f be homogeneous PartFunc of (X *),Y; :: thesis: dom f c= (arity f) -tuples_on X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in (arity f) -tuples_on X )
assume A1: x in dom f ; :: thesis: x in (arity f) -tuples_on X

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

suppose A2: X is empty ; :: thesis: x in (arity f) -tuples_on X

then x = <*> (X *) by A1, FUNCT_7:17, TARSKI:def 1;
then A3: arity f = len (<*> (X *)) by A1, MARGREL1:def 25;
0 -tuples_on X = {{}} by Th5;
hence x in (arity f) -tuples_on X by A1, A2, A3, FUNCT_7:17; :: thesis: verum

end;

suppose not X is empty ; :: thesis: x in (arity f) -tuples_on X

then reconsider X9 = X as non empty set ;
reconsider x9 = x as FinSequence of X9 by A1, FINSEQ_1:def 11;
len x9 = arity f by A1, MARGREL1:def 25;
then x9 is Element of (arity f) -tuples_on X9 by FINSEQ_2:92;
hence x in (arity f) -tuples_on X ; :: thesis: verum

end;

end;