let U1, U2 be Universal_Algebra; ( U1,U2 are_similar implies [:U1,U2:],U1 are_similar )
A1:
dom (signature U1) = Seg (len (signature U1))
by FINSEQ_1:def 3;
A2:
dom (signature U1) = Seg (len (signature U1))
by FINSEQ_1:def 3;
A3:
dom the charact of [:U1,U2:] = Seg (len the charact of [:U1,U2:])
by FINSEQ_1:def 3;
A4:
dom the charact of U2 = Seg (len the charact of U2)
by FINSEQ_1:def 3;
A5:
dom the charact of U1 = Seg (len the charact of U1)
by FINSEQ_1:def 3;
assume A6:
U1,U2 are_similar
; [:U1,U2:],U1 are_similar
then
[:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #)
by Def5;
then
len the charact of [:U1,U2:] = len the charact of U1
by A6, Def4;
then A7: len (signature [:U1,U2:]) =
len the charact of U1
by UNIALG_1:def 4
.=
len (signature U1)
by UNIALG_1:def 4
;
A8:
dom (signature [:U1,U2:]) = Seg (len (signature [:U1,U2:]))
by FINSEQ_1:def 3;
now for n being Nat st n in dom (signature U1) holds
(signature U1) . n = (signature [:U1,U2:]) . nlet n be
Nat;
( n in dom (signature U1) implies (signature U1) . n = (signature [:U1,U2:]) . n )assume A9:
n in dom (signature U1)
;
(signature U1) . n = (signature [:U1,U2:]) . nthen
n in dom the
charact of
[:U1,U2:]
by A7, A1, A3, UNIALG_1:def 4;
then reconsider o12 = the
charact of
[:U1,U2:] . n as
operation of
[:U1,U2:] by FUNCT_1:def 3;
len (signature U1) =
len (signature U2)
by A6
.=
len the
charact of
U2
by UNIALG_1:def 4
;
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A1, A4, A9, FUNCT_1:def 3;
A10:
o2 = the
charact of
U2 . n
;
A11:
n in Seg (len the charact of U1)
by A2, A9, UNIALG_1:def 4;
then
n in dom the
charact of
U1
by FINSEQ_1:def 3;
then reconsider o1 = the
charact of
U1 . n as
operation of
U1 by FUNCT_1:def 3;
(
(signature U1) . n = arity o1 &
(signature [:U1,U2:]) . n = arity o12 )
by A7, A1, A8, A9, UNIALG_1:def 4;
hence
(signature U1) . n = (signature [:U1,U2:]) . n
by A6, A5, A11, A10, Th5;
verum end;
hence
[:U1,U2:],U1 are_similar
by A7, FINSEQ_2:9; verum