let A be Universal_Algebra; :: thesis: ( Constants A = {} implies {} A is opers_closed )
assume A1: Constants A = {} ; :: thesis: {} A is opers_closed
let o be Element of Operations A; :: according to UNIALG_2:def 5 :: thesis: {} A is_closed_on o
let s be FinSequence of {} A; :: according to UNIALG_2:def 4 :: thesis: ( not len s = arity o or not o . s nin {} A )
assume A2: len s = arity o ; :: thesis: not o . s nin {} A
A3: rng s c= {} A by FINSEQ_1:def 4;
A4: s is Element of (arity o) -tuples_on the carrier of A by A2, FINSEQ_2:110;
dom o = (arity o) -tuples_on the carrier of A by MARGREL1:58;
then A5: o . s in rng o by A4, FUNCT_1:def 5;
then reconsider a = o . s as Element of A ;
a nin Constants A by A1;
then s <> {} by A2, A5, CARD_1:47;
hence not o . s nin {} A by A3; :: thesis: verum