let U1 be Universal_Algebra; :: thesis: for A being non empty Subset of U1
for o being operation of U1 st A is_closed_on o holds
arity (o /. A) = arity o
let A be non empty Subset of U1; :: thesis: for o being operation of U1 st A is_closed_on o holds
arity (o /. A) = arity o
let o be operation of U1; :: thesis: ( A is_closed_on o implies arity (o /. A) = arity o )
assume A is_closed_on o ; :: thesis: arity (o /. A) = arity o
then o /. A = o | ((arity o) -tuples_on A) by Def5;
then dom (o /. A) = (dom o) /\ ((arity o) -tuples_on A) by RELAT_1:61;
then A1: dom (o /. A) = ((arity o) -tuples_on the carrier of U1) /\ ((arity o) -tuples_on A) by MARGREL1:22
.= (arity o) -tuples_on A by MARGREL1:21 ;
dom (o /. A) = (arity (o /. A)) -tuples_on A by MARGREL1:22;
hence arity (o /. A) = arity o by A1, FINSEQ_2:110; :: thesis: verum