let U0 be Universal_Algebra; :: thesis: for H being non empty Subset of U0

for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

let H be non empty Subset of U0; :: thesis: for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

let o be operation of U0; :: thesis: ( arity o = 0 implies ( H is_closed_on o iff o . {} in H ) )

assume A1: arity o = 0 ; :: thesis: ( H is_closed_on o iff o . {} in H )

thus ( H is_closed_on o implies o . {} in H ) :: thesis: ( o . {} in H implies H is_closed_on o )

for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

let H be non empty Subset of U0; :: thesis: for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

let o be operation of U0; :: thesis: ( arity o = 0 implies ( H is_closed_on o iff o . {} in H ) )

assume A1: arity o = 0 ; :: thesis: ( H is_closed_on o iff o . {} in H )

thus ( H is_closed_on o implies o . {} in H ) :: thesis: ( o . {} in H implies H is_closed_on o )

proof

thus
( o . {} in H implies H is_closed_on o )
:: thesis: verum
assume A2:
H is_closed_on o
; :: thesis: o . {} in H

consider s being FinSequence of H such that

A3: len s = arity o by FINSEQ_1:19;

s = {} by A1, A3;

hence o . {} in H by A2, A3; :: thesis: verum

end;consider s being FinSequence of H such that

A3: len s = arity o by FINSEQ_1:19;

s = {} by A1, A3;

hence o . {} in H by A2, A3; :: thesis: verum

proof

assume A4:
o . {} in H
; :: thesis: H is_closed_on o

let s be FinSequence of H; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o or o . s in H )

assume len s = arity o ; :: thesis: o . s in H

then s = {} by A1;

hence o . s in H by A4; :: thesis: verum

end;let s be FinSequence of H; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o or o . s in H )

assume len s = arity o ; :: thesis: o . s in H

then s = {} by A1;

hence o . s in H by A4; :: thesis: verum