let A be non empty set ; :: thesis: for n being Nat
for f being Function of (n -tuples_on A),A holds
( f is non empty homogeneous quasi_total PartFunc of (A *),A & ( for g being homogeneous Function st f = g holds
g is n -ary ) )
let n be Nat; :: thesis: for f being Function of (n -tuples_on A),A holds
( f is non empty homogeneous quasi_total PartFunc of (A *),A & ( for g being homogeneous Function st f = g holds
g is n -ary ) )
let f be Function of (n -tuples_on A),A; :: thesis: ( f is non empty homogeneous quasi_total PartFunc of (A *),A & ( for g being homogeneous Function st f = g holds
g is n -ary ) )
A1: n in NAT by ORDINAL1:def 12;
then n -tuples_on A c= A * by FINSEQ_2:134;
then reconsider f = f as PartFunc of (A *),A by RELSET_1:7;
A2: dom f = n -tuples_on A by FUNCT_2:def 1;
then reconsider f = f as homogeneous PartFunc of (A *),A by A1, COMPUT_1:16;
set t = the Element of n -tuples_on A;
arity f = len the Element of n -tuples_on A by A2, MARGREL1:def 25
.= n by A1, FINSEQ_2:133 ;
hence ( f is non empty homogeneous quasi_total PartFunc of (A *),A & ( for g being homogeneous Function st f = g holds
g is n -ary ) ) by A2, COMPUT_1:def 21, COMPUT_1:22; :: thesis: verum