let U0, U1 be Universal_Algebra; :: thesis: for o0 being operation of U0
for o1 being operation of U1
for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds
arity o0 = arity o1
let o0 be operation of U0; :: thesis: for o1 being operation of U1
for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds
arity o0 = arity o1
let o1 be operation of U1; :: thesis: for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds
arity o0 = arity o1
let n be Nat; :: thesis: ( U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n implies arity o0 = arity o1 )
assume that
A1: U0 is SubAlgebra of U1 and
A2: ( n in dom the charact of U0 & o0 = the charact of U0 . n ) and
A3: o1 = the charact of U1 . n ; :: thesis: arity o0 = arity o1
reconsider A = the carrier of U0 as non empty Subset of U1 by A1, Def7;
A is opers_closed by A1, Def7;
then A4: A is_closed_on o1 ;
( n in dom (Opers (U1,A)) & o0 = (Opers (U1,A)) . n ) by A1, A2, Def7;
then o0 = o1 /. A by A3, Def6;
then o0 = o1 | ((arity o1) -tuples_on A) by A4, Def5;
then dom o0 = (dom o1) /\ ((arity o1) -tuples_on A) by RELAT_1:61;
then A5: dom o0 = ((arity o1) -tuples_on the carrier of U1) /\ ((arity o1) -tuples_on A) by MARGREL1:22
.= (arity o1) -tuples_on A by MARGREL1:21 ;
dom o0 = (arity o0) -tuples_on A by MARGREL1:22;
hence arity o0 = arity o1 by A5, FINSEQ_2:110; :: thesis: verum