set A = the non empty set ;

set a = the Element of the non empty set ;

reconsider w = (<*> the non empty set ) .--> the Element of the non empty set as Element of PFuncs (( the non empty set *), the non empty set ) by MARGREL1:19;

set U0 = UAStr(# the non empty set ,<*w*> #);

A1: ( the charact of UAStr(# the non empty set ,<*w*> #) is quasi_total & the charact of UAStr(# the non empty set ,<*w*> #) is homogeneous ) by MARGREL1:20;

the charact of UAStr(# the non empty set ,<*w*> #) is non-empty by MARGREL1:20;

then reconsider U0 = UAStr(# the non empty set ,<*w*> #) as Universal_Algebra by A1, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

take U0 ; :: thesis: ( U0 is with_const_op & U0 is strict )

( dom <*w*> = {1} & 1 in {1} ) by FINSEQ_1:2, FINSEQ_1:38, TARSKI:def 1;

then reconsider o = the charact of U0 . 1 as operation of U0 by FUNCT_1:def 3;

o = w by FINSEQ_1:40;

then A2: dom o = {(<*> the non empty set )} by FUNCOP_1:13;

then arity o = 0 by A2, A3, MARGREL1:def 25;

hence ( U0 is with_const_op & U0 is strict ) ; :: thesis: verum

set a = the Element of the non empty set ;

reconsider w = (<*> the non empty set ) .--> the Element of the non empty set as Element of PFuncs (( the non empty set *), the non empty set ) by MARGREL1:19;

set U0 = UAStr(# the non empty set ,<*w*> #);

A1: ( the charact of UAStr(# the non empty set ,<*w*> #) is quasi_total & the charact of UAStr(# the non empty set ,<*w*> #) is homogeneous ) by MARGREL1:20;

the charact of UAStr(# the non empty set ,<*w*> #) is non-empty by MARGREL1:20;

then reconsider U0 = UAStr(# the non empty set ,<*w*> #) as Universal_Algebra by A1, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

take U0 ; :: thesis: ( U0 is with_const_op & U0 is strict )

( dom <*w*> = {1} & 1 in {1} ) by FINSEQ_1:2, FINSEQ_1:38, TARSKI:def 1;

then reconsider o = the charact of U0 . 1 as operation of U0 by FUNCT_1:def 3;

o = w by FINSEQ_1:40;

then A2: dom o = {(<*> the non empty set )} by FUNCOP_1:13;

A3: now :: thesis: for x being FinSequence st x in dom o holds

len x = 0

<*> the non empty set in {(<*> the non empty set )}
by TARSKI:def 1;len x = 0

let x be FinSequence; :: thesis: ( x in dom o implies len x = 0 )

assume x in dom o ; :: thesis: len x = 0

then x = <*> the non empty set by A2, TARSKI:def 1;

hence len x = 0 ; :: thesis: verum

end;assume x in dom o ; :: thesis: len x = 0

then x = <*> the non empty set by A2, TARSKI:def 1;

hence len x = 0 ; :: thesis: verum

then arity o = 0 by A2, A3, MARGREL1:def 25;

hence ( U0 is with_const_op & U0 is strict ) ; :: thesis: verum