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;