let U0 be Universal_Algebra; :: thesis: for H being non empty Subset of U0
for o being operation of U0 st H is_closed_on o & arity o = 0 holds
o /. H = o
let H be non empty Subset of U0; :: thesis: for o being operation of U0 st H is_closed_on o & arity o = 0 holds
o /. H = o
let o be operation of U0; :: thesis: ( H is_closed_on o & arity o = 0 implies o /. H = o )
assume that
A1: H is_closed_on o and
A2: arity o = 0 ; :: thesis: o /. H = o
A3: dom o = 0 -tuples_on the carrier of U0 by A2, MARGREL1:22
.= {(<*> the carrier of U0)} by FINSEQ_2:94
.= {(<*> H)}
.= 0 -tuples_on H by FINSEQ_2:94 ;
o /. H = o | (0 -tuples_on H) by A1, A2, UNIALG_2:def 5;
hence o /. H = o by A3, RELAT_1:69; :: thesis: verum