let A be strict Universal_Algebra; for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
let a1, b1 be strict non-empty SubAlgebra of A; for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2
reconsider MSA = MSAlg (a1 "\/" b1) as MSSubAlgebra of MSAlg A by Th12;
let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 "\/" b1) = a2 "\/" b2 )
assume that
A1:
a2 = MSAlg a1
and
A2:
b2 = MSAlg b1
; MSAlg (a1 "\/" b1) = a2 "\/" b2
MSSign (a1 "\/" b1) = MSSign A
by Th7;
then reconsider MSA = MSA as strict non-empty MSSubAlgebra of MSAlg A ;
for B being MSSubset of (MSAlg A) st B = the Sorts of a2 (\/) the Sorts of b2 holds
MSA = GenMSAlg B
proof
( the
carrier of
a1 is
Subset of
A & the
carrier of
b1 is
Subset of
A )
by UNIALG_2:def 7;
then reconsider K = the
carrier of
a1 \/ the
carrier of
b1 as non
empty Subset of
A by XBOOLE_1:8;
reconsider ff1 =
(*--> 0) * (signature A) as
Function of
(dom (signature A)),
({0} *) by MSUALG_1:2;
set X =
MSA;
reconsider M1 = the
Sorts of
MSA as
ManySortedSet of the
carrier of
(MSSign A) ;
A3:
MSSign A = ManySortedSign(#
{0},
(dom (signature A)),
ff1,
((dom (signature A)) --> z) #)
by MSUALG_1:10;
then reconsider x =
0 as
Element of
(MSSign A) ;
let B be
MSSubset of
(MSAlg A);
( B = the Sorts of a2 (\/) the Sorts of b2 implies MSA = GenMSAlg B )
assume A4:
B = the
Sorts of
a2 (\/) the
Sorts of
b2
;
MSA = GenMSAlg B
A5:
for
U1 being
MSSubAlgebra of
MSAlg A st
B is
MSSubset of
U1 holds
MSA is
MSSubAlgebra of
U1
proof
let U1 be
MSSubAlgebra of
MSAlg A;
( B is MSSubset of U1 implies MSA is MSSubAlgebra of U1 )
assume A6:
B is
MSSubset of
U1
;
MSA is MSSubAlgebra of U1
per cases
( U1 is non-empty or not U1 is non-empty )
;
suppose
U1 is
non-empty
;
MSA is MSSubAlgebra of U1then reconsider U11 =
U1 as
non-empty MSSubAlgebra of
MSAlg A ;
A7:
1-Alg U11 is
SubAlgebra of
1-Alg (MSAlg A)
by Th20;
then reconsider A1 =
1-Alg U11 as
strict SubAlgebra of
A by MSUALG_1:9;
B c= the
Sorts of
U11
by A6, PBOOLE:def 18;
then A8:
B . x c= the
Sorts of
U11 . x
;
(
MSAlgebra(# the
Sorts of
U11, the
Charact of
U11 #)
= MSAlg (1-Alg U11) &
MSAlg (1-Alg U11) = MSAlgebra(#
(MSSorts (1-Alg U11)),
(MSCharact (1-Alg U11)) #) )
by A3, Th26, MSUALG_1:def 11;
then A9:
the
Sorts of
U11 . 0 = (0 .--> the carrier of (1-Alg U11)) . 0
by MSUALG_1:def 9;
B . 0 =
(0 .--> K) . 0
by A1, A2, A4, Th28
.=
K
by FUNCOP_1:72
;
then
the
carrier of
a1 \/ the
carrier of
b1 c= the
carrier of
A1
by A8, A9, FUNCOP_1:72;
then
GenUnivAlg K is
SubAlgebra of
1-Alg U11
by UNIALG_2:def 12;
then
a1 "\/" b1 is
SubAlgebra of
1-Alg U11
by UNIALG_2:def 13;
then A10:
MSA is
MSSubAlgebra of
MSAlg (1-Alg U11)
by Th12;
1-Alg U11 is
SubAlgebra of
A
by A7, MSUALG_1:9;
then
MSSign A = MSSign (1-Alg U11)
by Th7;
then
MSA is
MSSubAlgebra of
MSAlgebra(# the
Sorts of
U11, the
Charact of
U11 #)
by A3, A10, Th26;
hence
MSA is
MSSubAlgebra of
U1
by Th21;
verum end;
end;
MSA = MSAlgebra(#
(MSSorts (a1 "\/" b1)),
(MSCharact (a1 "\/" b1)) #)
by MSUALG_1:def 11;
then A14:
the
Sorts of
MSA = 0 .--> the
carrier of
(a1 "\/" b1)
by MSUALG_1:def 9;
the
Sorts of
a2 (\/) the
Sorts of
b2 c= M1
then
B is
MSSubset of
MSA
by A4, PBOOLE:def 18;
hence
MSA = GenMSAlg B
by A5, MSUALG_2:def 17;
verum
end;
hence
MSAlg (a1 "\/" b1) = a2 "\/" b2
by MSUALG_2:def 18; verum