let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies U1,U2 are_similar )
set s1 = signature U1;
set s2 = signature U2;
set X = dom (signature U1);
len (signature U1) = len the charact of U1 by UNIALG_1:def 4;
then A1: dom (signature U1) = dom the charact of U1 by FINSEQ_3:29;
assume A2: U1 is SubAlgebra of U2 ; :: thesis: U1,U2 are_similar
then reconsider A = the carrier of U1 as non empty Subset of U2 by Def7;
len (signature U2) = len the charact of U2 by UNIALG_1:def 4;
then A3: dom (signature U2) = dom the charact of U2 by FINSEQ_3:29;
dom the charact of U1 = dom (Opers (U2,A)) by A2, Def7;
then A4: dom (signature U1) = dom (signature U2) by A1, A3, Def6;
the charact of U1 = Opers (U2,A) by A2, Def7;
then A5: dom (signature U1) c= dom (signature U2) by A1, A3, Def6;
for n being Nat st n in dom (signature U1) holds
(signature U1) . n = (signature U2) . n

proof

let n be Nat; :: thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature U2) . n )
assume A6: n in dom (signature U1) ; :: thesis: (signature U1) . n = (signature U2) . n
then reconsider o1 = the charact of U1 . n as operation of U1 by A1, FUNCT_1:def 3;
reconsider o2 = the charact of U2 . n as operation of U2 by A3, A4, A6, FUNCT_1:def 3;
( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A5, A6, UNIALG_1:def 4;
hence (signature U1) . n = (signature U2) . n by A2, A1, A6, Th6; :: thesis: verum

end;

then signature U1 = signature U2 by A4, FINSEQ_1:13;
hence U1,U2 are_similar ; :: thesis: verum