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 4 :: thesis: ( len s = arity o implies o . s in B )
assume A3: len s = arity o ; :: thesis: o . s in B
A4: rng o c= B by A1, RELAT_1:def 19;
A5: dom o = (arity o) -tuples_on B by A1, Th2;
s is Element of (len s) -tuples_on B by FINSEQ_2:110;
then o . s in rng o by A3, A5, FUNCT_1:def 5;
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
A6: dom o = (arity o) -tuples_on B by A1, Th2;
o /. B = o | ((arity o) -tuples_on B) by A2, Def6;
hence o /. B = o by A6, RELAT_1:97; :: thesis: verum

end;

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