let U0 be Universal_Algebra; :: thesis: for B being non empty Subset of U0 st B = the carrier of U0 holds
( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )
let B be non empty Subset of U0; :: thesis: ( B = the carrier of U0 implies ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) )
assume A1: B = the carrier of U0 ; :: thesis: ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )
A2: for o being operation of U0 holds B is_closed_on o

proof

let o be operation of U0; :: thesis: B is_closed_on o
let s be FinSequence of B; :: according to UNIALG_2:def 3 :: thesis: ( len s = arity o implies o . s in B )
assume A3: len s = arity o ; :: thesis: o . s in B
( dom o = (arity o) -tuples_on B & s is Element of (len s) -tuples_on B ) by A1, FINSEQ_2:92, MARGREL1:22;
then A4: o . s in rng o by A3, FUNCT_1:def 3;
rng o c= B by A1, RELAT_1:def 19;
hence o . s in B by A4; :: thesis: verum

end;

for o being operation of U0 holds o /. B = o

proof

let o be operation of U0; :: thesis: o /. B = o
( dom o = (arity o) -tuples_on B & o /. B = o | ((arity o) -tuples_on B) ) by A1, A2, Def5, MARGREL1:22;
hence o /. B = o by RELAT_1:68; :: thesis: verum

end;

hence ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) by A2; :: thesis: verum