let A be with_empty-instruction Universal_Algebra; :: thesis: for o being Element of Operations A st o = Den ((In (1,(dom the charact of A))),A) holds
( arity o = 0 & EmptyIns A in rng o )
let o be Element of Operations A; :: thesis: ( o = Den ((In (1,(dom the charact of A))),A) implies ( arity o = 0 & EmptyIns A in rng o ) )
assume A1: o = Den ((In (1,(dom the charact of A))),A) ; :: thesis: ( arity o = 0 & EmptyIns A in rng o )
A2: dom (Den ((In (1,(dom the charact of A))),A)) = {{}} by Th42;
A3: <*> the carrier of A in {{}} by TARSKI:def 1;
hence arity o = len (<*> the carrier of A) by A1, A2, MARGREL1:def 25
.= 0 ;
:: thesis: EmptyIns A in rng o
thus EmptyIns A in rng o by A1, A2, A3, FUNCT_1:def 3; :: thesis: verum