set a = the Element of A;
reconsider f = (<*> A) .--> the Element of A as PartFunc of (A *),A by Th17;
reconsider f = f as Element of PFuncs ((A *),A) by PARTFUN1:45;
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 MARGREL1:def 23 :: 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 that
A1: n in dom <*f*> and
A2: h = <*f*> . n ; :: thesis: h is homogeneous
n in {1} by A1, FINSEQ_1:2, FINSEQ_1:def 8;
then h = <*f*> . 1 by A2, TARSKI:def 1;
then h = f ;
hence h is homogeneous ; :: thesis: verum

end;

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

proof

let n be Nat; :: according to MARGREL1:def 24 :: 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 that
A3: n in dom <*f*> and
A4: h = <*f*> . n ; :: thesis: h is quasi_total
n in {1} by A3, FINSEQ_1:2, FINSEQ_1:def 8;
then h = <*f*> . 1 by A4, TARSKI:def 1;
then h = f ;
hence h is quasi_total by Th17; :: thesis: verum

end;

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

proof

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

end;