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 )
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 dom f or b in dom f )
assume A3: len a = len b ; :: thesis: ( not a in dom f or b in dom f )
assume a in dom f ; :: thesis: b in dom f
then a = <*> X by TARSKI:def 1;
then b = {} by A3;
hence b in dom f by TARSKI:def 1; :: thesis: verum