let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) )
assume A1: U1,U2 are_similar ; :: thesis: for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
A2: dom (Opers U1,U2) = Seg (len (Opers U1,U2)) by FINSEQ_1:def 3;
A3: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def 3;
let o1 be operation of U1; :: thesis: for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let o2 be operation of U2; :: thesis: for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let o be operation of [:U1,U2:]; :: thesis: for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
let n be Nat; :: thesis: ( o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 implies ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) )
assume that
A4: o1 = the charact of U1 . n and
A5: o2 = the charact of U2 . n and
A6: o = the charact of [:U1,U2:] . n and
A7: n in dom the charact of U1 ; :: thesis: ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
A8: ( dom (signature U1) = Seg (len (signature U1)) & len (signature U1) = len the charact of U1 ) by FINSEQ_1:def 3, UNIALG_1:def 11;
then A9: (signature U1) . n = arity o1 by A4, A7, A3, UNIALG_1:def 11;
A10: signature U1 = signature U2 by A1, UNIALG_2:def 2;
then A11: (signature U2) . n = arity o2 by A5, A7, A3, A8, UNIALG_1:def 11;
A12: ( [:U1,U2:] = UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) & len the charact of U1 = len (Opers U1,U2) ) by A1, Def4, Def5;
then o = [[:o1,o2:]] by A1, A4, A5, A6, A7, A3, A2, Def4;
then A13: dom o = (arity o1) -tuples_on [:the carrier of U1,the carrier of U2:] by A10, A9, A11, Def3;
( ex x being FinSequence st x in dom o & ( for x being FinSequence st x in dom o holds
len x = arity o1 ) )

proof

consider a being Element of (arity o1) -tuples_on [:the carrier of U1,the carrier of U2:];
a in dom o by A13;
hence ex x being FinSequence st x in dom o ; :: thesis: for x being FinSequence st x in dom o holds
len x = arity o1
let x be FinSequence; :: thesis: ( x in dom o implies len x = arity o1 )
assume x in dom o ; :: thesis: len x = arity o1
then ex s being Element of [:the carrier of U1,the carrier of U2:] * st
( s = x & len s = arity o1 ) by A13;
hence len x = arity o1 ; :: thesis: verum

end;

hence ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) by A1, A4, A5, A6, A7, A3, A2, A12, A10, A9, A11, Def4, MARGREL1:def 26; :: thesis: verum