let U1, U2 be Universal_Algebra; :: thesis: ( 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 ; :: thesis: [: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 :: thesis: for n being Nat st n in dom (signature U1) holds
(signature U1) . n = (signature [:U1,U2:]) . n

let n be Nat; :: thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature [:U1,U2:]) . n )
assume A9: n in dom (signature U1) ; :: thesis: (signature U1) . n = (signature [:U1,U2:]) . n
then 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; :: thesis: verum

end;

hence [:U1,U2:],U1 are_similar by A7, FINSEQ_2:9; :: thesis: verum