let U1, U2 be Universal_Algebra; ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) )
assume A1:
U1 is SubAlgebra of U2
; for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
let B be MSSubset of (MSAlg U2); ( B = the Sorts of (MSAlg U1) implies the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) )
set f1 = the Charact of (MSAlg U1);
set f2 = Opers ((MSAlg U2),B);
the carrier' of (MSSign U1) = the carrier' of (MSSign U2)
proof
set ff1 =
(*--> 0) * (signature U1);
set ff2 =
(dom (signature U1)) --> z;
set gg1 =
(*--> 0) * (signature U2);
set gg2 =
(dom (signature U2)) --> z;
reconsider ff1 =
(*--> 0) * (signature U1) as
Function of
(dom (signature U1)),
({0} *) by MSUALG_1:2;
reconsider gg1 =
(*--> 0) * (signature U2) as
Function of
(dom (signature U2)),
({0} *) by MSUALG_1:2;
A2:
MSSign U2 = ManySortedSign(#
{0},
(dom (signature U2)),
gg1,
((dom (signature U2)) --> z) #)
by MSUALG_1:10;
(
U1,
U2 are_similar &
MSSign U1 = ManySortedSign(#
{0},
(dom (signature U1)),
ff1,
((dom (signature U1)) --> z) #) )
by A1, MSUALG_1:10, UNIALG_2:13;
hence
the
carrier' of
(MSSign U1) = the
carrier' of
(MSSign U2)
by A2;
verum
end;
then reconsider f1 = the Charact of (MSAlg U1) as ManySortedSet of the carrier' of (MSSign U2) ;
assume A3:
B = the Sorts of (MSAlg U1)
; the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
for x being object st x in the carrier' of (MSSign U2) holds
f1 . x = (Opers ((MSAlg U2),B)) . x
proof
let x be
object ;
( x in the carrier' of (MSSign U2) implies f1 . x = (Opers ((MSAlg U2),B)) . x )
assume A4:
x in the
carrier' of
(MSSign U2)
;
f1 . x = (Opers ((MSAlg U2),B)) . x
then reconsider y =
x as
OperSymbol of
(MSSign U2) ;
reconsider x =
x as
OperSymbol of
(MSSign U1) by A1, A4, Th7;
B is
opers_closed
by A1, A3, Th10;
then
(
(Opers ((MSAlg U2),B)) . y = y /. B &
B is_closed_on y )
by MSUALG_2:def 8;
then A5:
(Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . y)
by MSUALG_2:def 7;
((B #) * the Arity of (MSSign U1)) . x = (( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x
by A1, A3, Th7;
then
(Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | ((( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x)
by A1, A5, Th7;
then
(
f1 . x = Den (
x,
(MSAlg U1)) &
(Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (Args (x,(MSAlg U1))) )
by MSUALG_1:def 4, MSUALG_1:def 6;
hence
f1 . x = (Opers ((MSAlg U2),B)) . x
by A1, A3, Th8;
verum
end;
hence
the Charact of (MSAlg U1) = Opers ((MSAlg U2),B)
by PBOOLE:3; verum