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 = () --> 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 = () --> 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 = () --> x )

set f = () --> x;
A1: ( dom (() --> x) = n -tuples_on X & rng (() --> x) = {x} & n in omega ) by ;
then ( dom (() --> x) c= X * & rng (() --> x) c= X ) by ;
then reconsider f = () --> 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 ;
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 ;
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 = () --> 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 ;
the Element of n -tuples_on X in dom f ;
hence arity f = n by ; :: thesis: f = () --> x
thus f = () --> x ; :: thesis: verum