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