consider a being non empty homogeneous quasi_total PartFunc of (A * ),A;
reconsider a = a as Element of PFuncs (A * ),A by PARTFUN1:119;
take <*a*> ; :: thesis: ( <*a*> is homogeneous & <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )

hereby :: according to UNIALG_1:def 4 :: thesis: ( <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )

let n be Nat; :: thesis: for h being PartFunc of (A * ),A st n in dom <*a*> & h = <*a*> . n holds
h is homogeneous
let h be PartFunc of (A * ),A; :: thesis: ( n in dom <*a*> & h = <*a*> . n implies h is homogeneous )
assume n in dom <*a*> ; :: thesis: ( h = <*a*> . n implies h is homogeneous )
then n in Seg 1 by FINSEQ_1:55;
then n = 1 by FINSEQ_1:4, TARSKI:def 1;
hence ( h = <*a*> . n implies h is homogeneous ) by FINSEQ_1:57; :: thesis: verum

end;

hereby :: according to UNIALG_1:def 5 :: thesis: ( <*a*> is non-empty & not <*a*> is empty )

let n be Nat; :: thesis: for h being PartFunc of (A * ),A st n in dom <*a*> & h = <*a*> . n holds
h is quasi_total
let h be PartFunc of (A * ),A; :: thesis: ( n in dom <*a*> & h = <*a*> . n implies h is quasi_total )
assume n in dom <*a*> ; :: thesis: ( h = <*a*> . n implies h is quasi_total )
then n in Seg 1 by FINSEQ_1:55;
then n = 1 by FINSEQ_1:4, TARSKI:def 1;
hence ( h = <*a*> . n implies h is quasi_total ) by FINSEQ_1:57; :: thesis: verum

end;

hereby :: according to FUNCT_1:def 15 :: thesis: not <*a*> is empty

let n be set ; :: thesis: ( n in dom <*a*> implies not <*a*> . n is empty )
assume n in dom <*a*> ; :: thesis: not <*a*> . n is empty
then n in Seg 1 by FINSEQ_1:55;
then n = 1 by FINSEQ_1:4, TARSKI:def 1;
hence not <*a*> . n is empty by FINSEQ_1:57; :: thesis: verum

end;

thus not <*a*> is empty ; :: thesis: verum