consider x being Element of X;
set p = <*> X;
<*> X in X * by FINSEQ_1:def 11;
then reconsider Y = {(<*> X)} as Subset of (X * ) by ZFMISC_1:37;
( (<*> X) .--> x is homogeneous & Y --> x in PFuncs (X * ),X ) ;
then {(<*> X)} --> x in { f where f is Element of PFuncs (X * ),X : f is homogeneous } ;
then reconsider f = (<*> X) .--> x as Element of HFuncs X ;
take f ; :: thesis: ( not f is empty & f is homogeneous & f is quasi_total )
A1: 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 UNIALG_1:def 2 :: thesis: ( not len a = len b or not a in dom f or b in dom f )
assume A2: 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 A1, TARSKI:def 1;
then b = {} by A2;
hence b in dom f by A1, TARSKI:def 1; :: thesis: verum