consider A being non empty set ;
consider a being Element of A;
reconsider w = (<*> A) .--> a as Element of PFuncs (A * ),A by UNIALG_1:3;
set U0 = UAStr(# A,<*w*> #);
A1: ( the charact of UAStr(# A,<*w*> #) is quasi_total & the charact of UAStr(# A,<*w*> #) is homogeneous & the charact of UAStr(# A,<*w*> #) is non-empty ) by UNIALG_1:4;
reconsider U0 = UAStr(# A,<*w*> #) as Universal_Algebra by A1, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9;
take U0 ; :: thesis: ( U0 is with_const_op & U0 is strict )
( dom <*w*> = {1} & 1 in {1} ) by FINSEQ_1:4, FINSEQ_1:55, TARSKI:def 1;
then reconsider o = the charact of U0 . 1 as operation of U0 by FUNCT_1:def 5;
o = w by FINSEQ_1:57;
then A3: ( dom o = {(<*> A)} & <*> A in {(<*> A)} ) by FUNCOP_1:19, TARSKI:def 1;

now

let x be FinSequence; :: thesis: ( x in dom o implies len x = 0 )
assume x in dom o ; :: thesis: len x = 0
then x = <*> A by A3, TARSKI:def 1;
hence len x = 0 by FINSEQ_1:32; :: thesis: verum

end;

then arity o = 0 by A3, UNIALG_1:def 10;
hence ( U0 is with_const_op & U0 is strict ) by Def12; :: thesis: verum