let U0, U1 be Universal_Algebra; 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; 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; 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; ( 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
; 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; verum