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:]] )
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 A2: ( 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 ) ; :: thesis: ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
A3: [:U1,U2:] = UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) by A1, Def5;
A4: ( dom the charact of U1 = Seg (len the charact of U1) & dom the charact of U2 = Seg (len the charact of U2) & dom (Opers U1,U2) = Seg (len (Opers U1,U2)) & dom (signature U1) = Seg (len (signature U1)) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def 3;
A5: len the charact of U1 = len (Opers U1,U2) by A1, Def4;
then A6: o = [[:o1,o2:]] by A1, A2, A3, A4, Def4;
A7: signature U1 = signature U2 by A1, UNIALG_2:def 2;
( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def 11;
then A8: ( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A2, A4, A7, UNIALG_1:def 11;
then A9: dom o = (arity o1) -tuples_on [:the carrier of U1,the carrier of U2:] by A6, A7, 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 A9;
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 consider s being Element of [:the carrier of U1,the carrier of U2:] * such that
A10: ( s = x & len s = arity o1 ) by A9;
thus len x = arity o1 by A10; :: thesis: verum

end;

hence ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) by A1, A2, A3, A4, A5, A7, A8, Def4, UNIALG_1:def 10; :: thesis: verum