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 4;

then A9: (signature U1) . n = arity o1 by A4, A7, A3, UNIALG_1:def 4;

A10: signature U1 = signature U2 by A1;

then A11: (signature U2) . n = arity o2 by A5, A7, A3, A8, UNIALG_1:def 4;

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 ) )

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 4;

then A9: (signature U1) . n = arity o1 by A4, A7, A3, UNIALG_1:def 4;

A10: signature U1 = signature U2 by A1;

then A11: (signature U2) . n = arity o2 by A5, A7, A3, A8, UNIALG_1:def 4;

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

hence
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )
by A1, A4, A5, A6, A7, A3, A2, A12, A9, A11, Def4, MARGREL1:def 25; :: thesis: verum
set a = the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:];

the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] 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;the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] 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