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 A1: ( U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n ) ; :: thesis: arity o0 = arity o1
then reconsider A = the carrier of U0 as non empty Subset of U1 by Def8;
A is opers_closed by A1, Def8;
then A2: A is_closed_on o1 by Def5;
A3: n in dom (Opers U1,A) by A1, Def8;
o0 = (Opers U1,A) . n by A1, Def8;
then o0 = o1 /. A by A1, A3, Def7;
then o0 = o1 | ((arity o1) -tuples_on A) by A2, Def6;
then dom o0 = (dom o1) /\ ((arity o1) -tuples_on A) by RELAT_1:90;
then A4: dom o0 = ((arity o1) -tuples_on the carrier of U1) /\ ((arity o1) -tuples_on A) by Th2
.= (arity o1) -tuples_on A by Th1 ;
dom o0 = (arity o0) -tuples_on A by Th2;
hence arity o0 = arity o1 by A4, FINSEQ_2:130; :: thesis: verum