set p = <*> X;
set x = the Element of X;
<*> X in X * by FINSEQ_1:def 11;
then reconsider Y = {(<*> X)} as Subset of (X *) by ZFMISC_1:31;
A1: Y --> the Element of X in PFuncs ((X *),X) ;
(<*> X) .--> the Element of X is homogeneous ;
then {(<*> X)} --> the Element of X in { f where f is Element of PFuncs ((X *),X) : f is homogeneous } by A1;
then reconsider f = (<*> X) .--> the Element of 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:13;
thus ( not f is empty & f is homogeneous ) ; :: thesis: f is quasi_total
let a, b be FinSequence of X; :: according to MARGREL1:def 22 :: 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