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

( 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

for o being operation of U0 holds o /. B = o
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;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

proof

hence
( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )
by A2; :: thesis: verum
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;( 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