let A be non empty set ; :: thesis:
let a be Element of A; :: thesis:
let x be Element of PFuncs ((A *),A); :: thesis:
assume A1: x = (<*> A) .--> a ; :: thesis:
A2: for n being Nat
for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds
h is homogeneous

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

end;

A5: for n being Nat
for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds
h is quasi_total

let n be Nat; :: thesis:
let h be PartFunc of (A *),A; :: thesis:
assume that
A6: n in dom <*x*> and
A7: h = <*x*> . n ; :: thesis:
n in {1} by A6, FINSEQ_1:2, FINSEQ_1:def 8;
then h = <*x*> . 1 by A7, TARSKI:def 1;
then h = x by FINSEQ_1:def 8;
hence h is quasi_total by A1, Th17; :: thesis:

end;

for n being object st n in dom <*x*> holds
not <*x*> . n is empty

let n be object ; :: thesis:
assume n in dom <*x*> ; :: thesis:
then n in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then <*x*> . n = <*x*> . 1 by TARSKI:def 1;
hence not <*x*> . n is empty by A1, FINSEQ_1:def 8; :: thesis:

end;

hence ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) by A2, A5, FUNCT_1:def 9; :: thesis: