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 4 :: thesis: {} A is_closed_on o
let s be FinSequence of {} A; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o or o . s in {} A )
assume A2: len s = arity o ; :: thesis: o . s in {} A
A3: s is Element of (arity o) -tuples_on the carrier of A by A2, FINSEQ_2:92;
dom o = (arity o) -tuples_on the carrier of A by MARGREL1:22;
then A4: o . s in rng o by A3, FUNCT_1:def 3;
then reconsider a = o . s as Element of A ;
a nin Constants A by A1;
then s <> {} by A2, A4;
hence o . s in {} A ; :: thesis: verum