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

hence U1,U2 are_similar ; :: thesis: verum

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

then
signature U1 = signature U2
by A4, FINSEQ_1:13;
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;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

hence U1,U2 are_similar ; :: thesis: verum