let U1, U2 be Universal_Algebra; :: thesis: ( 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
; :: thesis: 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); :: thesis: ( B = the Sorts of (MSAlg U1) implies the Charact of (MSAlg U1) = Opers (MSAlg U2),B )
assume A2:
B = the Sorts of (MSAlg U1)
; :: thesis: 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
A3:
U1,
U2 are_similar
by A1, UNIALG_2:16;
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:7;
reconsider gg1 =
(*--> 0 ) * (signature U2) as
Function of
(dom (signature U2)),
({0 } * ) by MSUALG_1:7;
A4:
MSSign U1 = ManySortedSign(#
{0 },
(dom (signature U1)),
ff1,
((dom (signature U1)) --> z) #)
by MSUALG_1:16;
MSSign U2 = ManySortedSign(#
{0 },
(dom (signature U2)),
gg1,
((dom (signature U2)) --> z) #)
by MSUALG_1:16;
hence
the
carrier' of
(MSSign U1) = the
carrier' of
(MSSign U2)
by A3, A4, UNIALG_2:def 2;
:: thesis: verum
end;
then reconsider f1 = the Charact of (MSAlg U1) as ManySortedSet of ;
for x being set st x in the carrier' of (MSSign U2) holds
f1 . x = (Opers (MSAlg U2),B) . x
proof
let x be
set ;
:: thesis: ( x in the carrier' of (MSSign U2) implies f1 . x = (Opers (MSAlg U2),B) . x )
assume A5:
x in the
carrier' of
(MSSign U2)
;
:: thesis: 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, A5, Th7;
A6:
f1 . x = Den x,
(MSAlg U1)
by MSUALG_1:def 11;
A7:
(Opers (MSAlg U2),B) . y = y /. B
by MSUALG_2:def 9;
B is
opers_closed
by A1, A2, Th10;
then
B is_closed_on y
by MSUALG_2:def 7;
then A8:
(Opers (MSAlg U2),B) . y = (Den y,(MSAlg U2)) | (((B # ) * the Arity of (MSSign U2)) . y)
by A7, MSUALG_2:def 8;
((B # ) * the Arity of (MSSign U1)) . x = ((the Sorts of (MSAlg U1) # ) * the Arity of (MSSign U1)) . x
by A1, A2, Th7;
then
(Opers (MSAlg U2),B) . y = (Den y,(MSAlg U2)) | (((the Sorts of (MSAlg U1) # ) * the Arity of (MSSign U1)) . x)
by A1, A8, Th7;
then
(Opers (MSAlg U2),B) . y = (Den y,(MSAlg U2)) | (Args x,(MSAlg U1))
by MSUALG_1:def 9;
hence
f1 . x = (Opers (MSAlg U2),B) . x
by A1, A2, A6, Th8;
:: thesis: verum
end;
hence
the Charact of (MSAlg U1) = Opers (MSAlg U2),B
by PBOOLE:3; :: thesis: verum