let A be non empty set ; :: thesis: for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A)
let a be Element of A; :: thesis: (<*> A) .--> a is Element of PFuncs ((A *),A)
set f = (<*> A) .--> a;
A2: dom ((<*> A) .--> a) c= A *

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom ((<*> A) .--> a) or z in A * )
assume z in dom ((<*> A) .--> a) ; :: thesis: z in A *
then z = <*> A by TARSKI:def 1;
hence z in A * by FINSEQ_1:def 11; :: thesis: verum

end;

A3: rng ((<*> A) .--> a) = {a} by FUNCOP_1:8;
rng ((<*> A) .--> a) c= A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng ((<*> A) .--> a) or z in A )
assume z in rng ((<*> A) .--> a) ; :: thesis: z in A
then z = a by A3, TARSKI:def 1;
hence z in A ; :: thesis: verum

end;

then reconsider f = (<*> A) .--> a as PartFunc of (A *),A by A2, RELSET_1:4;
f in PFuncs ((A *),A) by PARTFUN1:45;
hence (<*> A) .--> a is Element of PFuncs ((A *),A) ; :: thesis: verum