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

proof

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

end;

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

proof

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

end;

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

proof

let n be set ; :: thesis: ( n in dom <*x*> implies not <*x*> . n is empty )
assume n in dom <*x*> ; :: thesis: not <*x*> . n is empty
then n in {1} by FINSEQ_1:4, 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: verum

end;

hence ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) by A2, A4, Def4, Def5, FUNCT_1:def 15; :: thesis: verum