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: ( {} A c= the carrier of A & rng s c= {} A ) by FINSEQ_1:def 4;
( s is Element of (arity o) -tuples_on the carrier of A & dom o = (arity o) -tuples_on the carrier of A ) by A2, FINSEQ_2:110, UNIALG_2:2;
then A4: o . s in rng o by FUNCT_1:def 5;
then reconsider a = o . s as Element of A ;
a nin Constants A by A1;
then s <> {} by A2, A4, CARD_1:47;
hence not o . s nin {} A by A3; :: thesis: verum