let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies [:U1,U2:],U1 are_similar )
A1: dom () = Seg (len ()) by FINSEQ_1:def 3;
A2: dom () = Seg (len ()) 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 ;
then A7: len (signature [:U1,U2:]) = len the charact of U1 by UNIALG_1:def 4
.= len () 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 () holds
() . n = (signature [:U1,U2:]) . n
let n be Nat; :: thesis: ( n in dom () implies () . n = (signature [:U1,U2:]) . n )
assume A9: n in dom () ; :: thesis: () . n = (signature [:U1,U2:]) . n
then n in dom the charact of [:U1,U2:] by ;
then reconsider o12 = the charact of [:U1,U2:] . n as operation of [:U1,U2:] by FUNCT_1:def 3;
len () = len () 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 ;
A10: o2 = the charact of U2 . n ;
A11: n in Seg (len the charact of U1) by ;
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 ;
hence (signature U1) . n = (signature [:U1,U2:]) . n by A6, A5, A11, A10, Th5; :: thesis: verum
end;
hence [:U1,U2:],U1 are_similar by ; :: thesis: verum