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 )
proof
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;
thus ( o . {} in H implies H is_closed_on o ) :: 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;