let A be non empty set ; :: thesis: for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A * ),A
let a be Element of A; :: thesis: (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A * ),A
set f = (<*> A) .--> a;
A1: ( dom ((<*> A) .--> a) = {(<*> A)} & rng ((<*> A) .--> a) = {a} ) by FUNCOP_1:14, FUNCOP_1:19;
A2: dom ((<*> A) .--> a) c= A *

proof

let z be set ; :: 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 A1, TARSKI:def 1;
hence z in A * by FINSEQ_1:def 11; :: thesis: verum

end;

rng ((<*> A) .--> a) c= A

proof

let z be set ; :: 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 A1, TARSKI:def 1;
hence z in A ; :: thesis: verum

end;

then reconsider f = (<*> A) .--> a as PartFunc of (A * ),A by A2, RELSET_1:11;
A3: f is homogeneous

proof

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( x in dom f & y in dom f implies len x = len y )
assume ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then ( x = <*> A & y = <*> A ) by A1, TARSKI:def 1;
hence len x = len y ; :: thesis: verum

end;

f is quasi_total

proof

let x, y be FinSequence of A; :: according to UNIALG_1:def 2 :: thesis: ( len x = len y & x in dom f implies y in dom f )
assume A4: ( len x = len y & x in dom f ) ; :: thesis: y in dom f
then x = <*> A by A1, TARSKI:def 1;
then len x = 0 by FINSEQ_1:32;
then y = <*> A by A4, FINSEQ_1:32;
hence y in dom f by A1, TARSKI:def 1; :: thesis: verum

end;

hence (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A * ),A by A3; :: thesis: verum