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

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