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 ();
len () = len the charact of U1 by UNIALG_1:def 4;
then A1: dom () = 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 () = len the charact of U2 by UNIALG_1:def 4;
then A3: dom () = dom the charact of U2 by FINSEQ_3:29;
dom the charact of U1 = dom (Opers (U2,A)) by ;
then A4: dom () = dom () by A1, A3, Def6;
the charact of U1 = Opers (U2,A) by ;
then A5: dom () c= dom () by A1, A3, Def6;
for n being Nat st n in dom () holds
() . n = () . n
proof
let n be Nat; :: thesis: ( n in dom () implies () . n = () . n )
assume A6: n in dom () ; :: thesis: () . n = () . n
then reconsider o1 = the charact of U1 . n as operation of U1 by ;
reconsider o2 = the charact of U2 . n as operation of U2 by ;
( (signature U1) . n = arity o1 & () . n = arity o2 ) by ;
hence (signature U1) . n = () . n by A2, A1, A6, Th6; :: thesis: verum
end;
then signature U1 = signature U2 by ;
hence U1,U2 are_similar ; :: thesis: verum