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

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