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

proof

let n be Nat; :: according to UNIALG_1:def 4 :: thesis: for h being PartFunc of (A * ),A st n in dom <*f*> & h = <*f*> . n holds
h is homogeneous
let h be PartFunc of (A * ),A; :: thesis: ( n in dom <*f*> & h = <*f*> . n implies h is homogeneous )
assume A1: ( n in dom <*f*> & h = <*f*> . n ) ; :: thesis: h is homogeneous
then n in {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then h = <*f*> . 1 by A1, TARSKI:def 1;
then ( h = f & f is homogeneous PartFunc of (A * ),A ) by Th2, FINSEQ_1:def 8;
hence h is homogeneous ; :: thesis: verum

end;

thus <*f*> is quasi_total :: thesis: <*f*> is non-empty

proof

let n be Nat; :: according to UNIALG_1:def 5 :: thesis: for h being PartFunc of (A * ),A st n in dom <*f*> & h = <*f*> . n holds
h is quasi_total
let h be PartFunc of (A * ),A; :: thesis: ( n in dom <*f*> & h = <*f*> . n implies h is quasi_total )
assume A2: ( n in dom <*f*> & h = <*f*> . n ) ; :: thesis: h is quasi_total
then n in {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then h = <*f*> . 1 by A2, TARSKI:def 1;
then ( h = f & f is quasi_total PartFunc of (A * ),A ) by Th2, FINSEQ_1:def 8;
hence h is quasi_total ; :: thesis: verum

end;

thus <*f*> is non-empty :: thesis: verum

proof

let n be set ; :: according to FUNCT_1:def 15 :: thesis: ( not n in dom <*f*> or not <*f*> . n is empty )
assume A3: n in dom <*f*> ; :: thesis: not <*f*> . n is empty
then reconsider n = n as Element of NAT ;
n in {1} by A3, FINSEQ_1:4, FINSEQ_1:def 8;
then n = 1 by TARSKI:def 1;
hence not <*f*> . n is empty by FINSEQ_1:def 8; :: thesis: verum

end;