consider o being operation of A such that
A1: arity o = 0 by UNIALG_2:def 11;
reconsider oo = o as operation of UAStr(# the carrier of A, the charact of A #) ;
take oo ; :: according to UNIALG_2:def 11 :: thesis: arity oo = 0
thus arity oo = 0 by A1; :: thesis: verum