set a = the Element of A;
set f = (<*> A) .--> the Element of A;
A2: dom ((<*> A) .--> the Element of A) c= A *

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom ((<*> A) .--> the Element of A) or z in A * )
assume z in dom ((<*> A) .--> the Element of 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) .--> the Element of A) = { the Element of A} by FUNCOP_1:8;
rng ((<*> A) .--> the Element of A) c= A

proof

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

end;

then reconsider f = (<*> A) .--> the Element of A as PartFunc of (A *),A by A2, RELSET_1:4;
A4: f is quasi_total

proof

let x, y be FinSequence of A; :: according to MARGREL1:def 22 :: thesis: ( len x = len y & x in dom f implies y in dom f )
assume that
A5: len x = len y and
A6: x in dom f ; :: thesis: y in dom f
x = <*> A by A6, TARSKI:def 1;
then len x = 0 ;
then y = <*> A by A5;
hence y in dom f by TARSKI:def 1; :: thesis: verum

end;

f is homogeneous ;
hence ex b₁ being PartFunc of (A *),A st
( b₁ is homogeneous & b₁ is quasi_total & not b₁ is empty ) by A4; :: thesis: verum