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:
thus <*f*> is homogeneous :: thesis:

let n be Nat; :: according to MARGREL1:def 23 :: thesis:
let h be PartFunc of (A *),A; :: thesis:
assume that
A1: n in dom <*f*> and
A2: h = <*f*> . n ; :: thesis:
n in {1} by A1, FINSEQ_1:2, FINSEQ_1:def 8;
then h = <*f*> . 1 by A2, TARSKI:def 1;
then h = f by FINSEQ_1:def 8;
hence h is homogeneous ; :: thesis:

end;

thus <*f*> is quasi_total :: thesis:

let n be Nat; :: according to MARGREL1:def 24 :: thesis:
let h be PartFunc of (A *),A; :: thesis:
assume that
A3: n in dom <*f*> and
A4: h = <*f*> . n ; :: thesis:
n in {1} by A3, FINSEQ_1:2, FINSEQ_1:def 8;
then h = <*f*> . 1 by A4, TARSKI:def 1;
then h = f by FINSEQ_1:def 8;
hence h is quasi_total by Th17; :: thesis:

end;

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

let n be object ; :: according to FUNCT_1:def 9 :: thesis:
assume A5: n in dom <*f*> ; :: thesis:
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 by FINSEQ_1:def 8; :: thesis:

end;