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 26
.= 0 ;
:: thesis: EmptyIns A in rng o
thus EmptyIns A in rng o by A1, A2, A3, FUNCT_1:def 5; :: thesis: verum