let n be natural number ; :: thesis: for X being non empty set
for x being Element of X ex f being non empty homogeneous quasi_total PartFunc of (X *),X st
( arity f = n & f = (n -tuples_on X) --> x )
let X be non empty set ; :: thesis: for x being Element of X ex f being non empty homogeneous quasi_total PartFunc of (X *),X st
( arity f = n & f = (n -tuples_on X) --> x )
let x be Element of X; :: thesis: ex f being non empty homogeneous quasi_total PartFunc of (X *),X st
( arity f = n & f = (n -tuples_on X) --> x )
set f = (n -tuples_on X) --> x;
A1: ( dom ((n -tuples_on X) --> x) = n -tuples_on X & rng ((n -tuples_on X) --> x) = {x} & n in omega ) by FUNCOP_1:8, ORDINAL1:def 12;
then ( dom ((n -tuples_on X) --> x) c= X * & rng ((n -tuples_on X) --> x) c= X ) by ZFMISC_1:31, FINSEQ_2:134;
then reconsider f = (n -tuples_on X) --> x as non empty PartFunc of (X *),X by RELSET_1:4;
A2: f is quasi_total
proof
let x, y be FinSequence of X; :: according to MARGREL1:def 22 :: thesis: ( not len x = len y or not x in dom f or y in dom f )
assume ( len x = len y & x in dom f ) ; :: thesis: y in dom f
then ( len x = n & len y = n ) by A1, FINSEQ_2:132;
hence y in dom f by FINSEQ_2:133; :: thesis: verum
end;
f is homogeneous
proof
let x, y be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis: ( not x in dom f or not y in dom f or len x = len y )
assume ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then reconsider x = x, y = y as Element of n -tuples_on X ;
( len x = n & len y = n ) by A1, FINSEQ_2:132;
hence len x = len y ; :: thesis: verum
end;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (X *),X by A2;
take f ; :: thesis: ( arity f = n & f = (n -tuples_on X) --> x )
set y = the Element of n -tuples_on X;
A3: for x being FinSequence st x in dom f holds
n = len x by A1, FINSEQ_2:132;
the Element of n -tuples_on X in dom f ;
hence arity f = n by A3, MARGREL1:def 25; :: thesis: f = (n -tuples_on X) --> x
thus f = (n -tuples_on X) --> x ; :: thesis: verum