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

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