set p = <*> X;
consider x being Element of X;
<*> X in X * by FINSEQ_1:def 11;
then reconsider Y = {(<*> X)} as Subset of (X * ) by ZFMISC_1:37;
A1: Y --> x in PFuncs (X * ),X ;
(<*> X) .--> x is homogeneous ;
then {(<*> X)} --> x in { f where f is Element of PFuncs (X * ),X : f is homogeneous } by A1;
then reconsider f = (<*> X) .--> x as Element of HFuncs X ;
take f ; :: thesis: ( not f is empty & f is homogeneous & f is quasi_total )
A2: dom f = {(<*> X)} by FUNCOP_1:19;
thus ( not f is empty & f is homogeneous ) ; :: thesis: f is quasi_total
let a, b be FinSequence of X; :: according to MARGREL1:def 23 :: thesis: ( not len a = len b or not a in proj1 f or b in proj1 f )
assume A3: len a = len b ; :: thesis: ( not a in proj1 f or b in proj1 f )
assume a in dom f ; :: thesis: b in proj1 f
then a = <*> X by A2, TARSKI:def 1;
then b = {} by A3;
hence b in proj1 f by A2, TARSKI:def 1; :: thesis: verum