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;

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

hence
[:U1,U2:],U1 are_similar
by A7, FINSEQ_2:9; :: thesis: verum(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;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