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:
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 = () -tuples_on B & s is Element of (len s) -tuples_on B ) by ;
then A4: o . s in rng o by ;
rng o c= B by ;
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 = () -tuples_on B & o /. B = o | (() -tuples_on B) ) by ;
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