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 )
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 that
A3: n in dom <*x*> and
A4: h = <*x*> . n ; :: thesis: h is homogeneous
n in {1} by A3, FINSEQ_1:4, 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, Th54; :: thesis: verum

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

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 that
A6: n in dom <*x*> and
A7: h = <*x*> . n ; :: thesis: h is quasi_total
n in {1} by A6, FINSEQ_1:4, 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, Th54; :: 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, A5, Def4, Def5, FUNCT_1:def 15; :: thesis: verum
reconsider f = x as PartFunc of (A * ),A by PARTFUN1:121;