:: MSUALG_4 semantic presentation
:: deftheorem Def1 defines Relation-yielding MSUALG_4:def 1 :
:: deftheorem Def2 defines ManySortedRelation MSUALG_4:def 2 :
:: deftheorem Def3 defines MSEquivalence_Relation-like MSUALG_4:def 3 :
:: deftheorem Def4 MSUALG_4:def 4 :
canceled;
:: deftheorem Def5 defines MSEquivalence-like MSUALG_4:def 5 :
theorem Th1: :: MSUALG_4:1
:: deftheorem Def6 defines MSCongruence-like MSUALG_4:def 6 :
:: deftheorem Def7 defines Class MSUALG_4:def 7 :
:: deftheorem Def8 defines Class MSUALG_4:def 8 :
:: deftheorem Def9 defines # MSUALG_4:def 9 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2 be
OperSymbol of
c1;
let c3 be
non-empty MSAlgebra of
c1;
let c4 be
MSCongruence of
c3;
func QuotRes c4,
c2 -> Function of
(the Sorts of a3 * the ResultSort of a1) . a2,
((Class a4) * the ResultSort of a1) . a2 means :
Def10:
:: MSUALG_4:def 10
for
b1 being
Element of the
Sorts of
a3 . (the_result_sort_of a2) holds
a5 . b1 = Class a4,
b1;
existence
ex b1 being Function of (the Sorts of c3 * the ResultSort of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st
for b2 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b1 . b2 = Class c4,b2
uniqueness
for b1, b2 being Function of (the Sorts of c3 * the ResultSort of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st ( for b3 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b1 . b3 = Class c4,b3 ) & ( for b3 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b2 . b3 = Class c4,b3 ) holds
b1 = b2
func QuotArgs c4,
c2 -> Function of
((the Sorts of a3 # ) * the Arity of a1) . a2,
(((Class a4) # ) * the Arity of a1) . a2 means :: MSUALG_4:def 11
for
b1 being
Element of
Args a2,
a3 holds
a5 . b1 = a4 # b1;
existence
ex b1 being Function of ((the Sorts of c3 # ) * the Arity of c1) . c2,(((Class c4) # ) * the Arity of c1) . c2 st
for b2 being Element of Args c2,c3 holds b1 . b2 = c4 # b2
uniqueness
for b1, b2 being Function of ((the Sorts of c3 # ) * the Arity of c1) . c2,(((Class c4) # ) * the Arity of c1) . c2 st ( for b3 being Element of Args c2,c3 holds b1 . b3 = c4 # b3 ) & ( for b3 being Element of Args c2,c3 holds b2 . b3 = c4 # b3 ) holds
b1 = b2
end;
:: deftheorem Def10 defines QuotRes MSUALG_4:def 10 :
:: deftheorem Def11 defines QuotArgs MSUALG_4:def 11 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2 be
non-empty MSAlgebra of
c1;
let c3 be
MSCongruence of
c2;
func QuotRes c3 -> ManySortedFunction of the
Sorts of
a2 * the
ResultSort of
a1,
(Class a3) * the
ResultSort of
a1 means :: MSUALG_4:def 12
for
b1 being
OperSymbol of
a1 holds
a4 . b1 = QuotRes a3,
b1;
existence
ex b1 being ManySortedFunction of the Sorts of c2 * the ResultSort of c1,(Class c3) * the ResultSort of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = QuotRes c3,b2
uniqueness
for b1, b2 being ManySortedFunction of the Sorts of c2 * the ResultSort of c1,(Class c3) * the ResultSort of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = QuotRes c3,b3 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = QuotRes c3,b3 ) holds
b1 = b2
func QuotArgs c3 -> ManySortedFunction of
(the Sorts of a2 # ) * the
Arity of
a1,
((Class a3) # ) * the
Arity of
a1 means :: MSUALG_4:def 13
for
b1 being
OperSymbol of
a1 holds
a4 . b1 = QuotArgs a3,
b1;
existence
ex b1 being ManySortedFunction of (the Sorts of c2 # ) * the Arity of c1,((Class c3) # ) * the Arity of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = QuotArgs c3,b2
uniqueness
for b1, b2 being ManySortedFunction of (the Sorts of c2 # ) * the Arity of c1,((Class c3) # ) * the Arity of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = QuotArgs c3,b3 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = QuotArgs c3,b3 ) holds
b1 = b2
end;
:: deftheorem Def12 defines QuotRes MSUALG_4:def 12 :
:: deftheorem Def13 defines QuotArgs MSUALG_4:def 13 :
theorem Th2: :: MSUALG_4:2
definition
let c1 be non
empty non
void ManySortedSign ;
let c2 be
OperSymbol of
c1;
let c3 be
non-empty MSAlgebra of
c1;
let c4 be
MSCongruence of
c3;
func QuotCharact c4,
c2 -> Function of
(((Class a4) # ) * the Arity of a1) . a2,
((Class a4) * the ResultSort of a1) . a2 means :
Def14:
:: MSUALG_4:def 14
for
b1 being
Element of
Args a2,
a3 st
a4 # b1 in (((Class a4) # ) * the Arity of a1) . a2 holds
a5 . (a4 # b1) = ((QuotRes a4,a2) * (Den a2,a3)) . b1;
existence
ex b1 being Function of (((Class c4) # ) * the Arity of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st
for b2 being Element of Args c2,c3 st c4 # b2 in (((Class c4) # ) * the Arity of c1) . c2 holds
b1 . (c4 # b2) = ((QuotRes c4,c2) * (Den c2,c3)) . b2
uniqueness
for b1, b2 being Function of (((Class c4) # ) * the Arity of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st ( for b3 being Element of Args c2,c3 st c4 # b3 in (((Class c4) # ) * the Arity of c1) . c2 holds
b1 . (c4 # b3) = ((QuotRes c4,c2) * (Den c2,c3)) . b3 ) & ( for b3 being Element of Args c2,c3 st c4 # b3 in (((Class c4) # ) * the Arity of c1) . c2 holds
b2 . (c4 # b3) = ((QuotRes c4,c2) * (Den c2,c3)) . b3 ) holds
b1 = b2
end;
:: deftheorem Def14 defines QuotCharact MSUALG_4:def 14 :
:: deftheorem Def15 defines QuotCharact MSUALG_4:def 15 :
:: deftheorem Def16 defines QuotMSAlg MSUALG_4:def 16 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2 be
non-empty MSAlgebra of
c1;
let c3 be
MSCongruence of
c2;
let c4 be
SortSymbol of
c1;
func MSNat_Hom c2,
c3,
c4 -> Function of the
Sorts of
a2 . a4,
(Class a3) . a4 means :
Def17:
:: MSUALG_4:def 17
for
b1 being
set st
b1 in the
Sorts of
a2 . a4 holds
a5 . b1 = Class (a3 . a4),
b1;
existence
ex b1 being Function of the Sorts of c2 . c4,(Class c3) . c4 st
for b2 being set st b2 in the Sorts of c2 . c4 holds
b1 . b2 = Class (c3 . c4),b2
uniqueness
for b1, b2 being Function of the Sorts of c2 . c4,(Class c3) . c4 st ( for b3 being set st b3 in the Sorts of c2 . c4 holds
b1 . b3 = Class (c3 . c4),b3 ) & ( for b3 being set st b3 in the Sorts of c2 . c4 holds
b2 . b3 = Class (c3 . c4),b3 ) holds
b1 = b2
end;
:: deftheorem Def17 defines MSNat_Hom MSUALG_4:def 17 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2 be
non-empty MSAlgebra of
c1;
let c3 be
MSCongruence of
c2;
func MSNat_Hom c2,
c3 -> ManySortedFunction of
a2,
(QuotMSAlg a2,a3) means :
Def18:
:: MSUALG_4:def 18
for
b1 being
SortSymbol of
a1 holds
a4 . b1 = MSNat_Hom a2,
a3,
b1;
existence
ex b1 being ManySortedFunction of c2,(QuotMSAlg c2,c3) st
for b2 being SortSymbol of c1 holds b1 . b2 = MSNat_Hom c2,c3,b2
uniqueness
for b1, b2 being ManySortedFunction of c2,(QuotMSAlg c2,c3) st ( for b3 being SortSymbol of c1 holds b1 . b3 = MSNat_Hom c2,c3,b3 ) & ( for b3 being SortSymbol of c1 holds b2 . b3 = MSNat_Hom c2,c3,b3 ) holds
b1 = b2
end;
:: deftheorem Def18 defines MSNat_Hom MSUALG_4:def 18 :
theorem Th3: :: MSUALG_4:3
definition
let c1 be non
empty non
void ManySortedSign ;
let c2,
c3 be
non-empty MSAlgebra of
c1;
let c4 be
ManySortedFunction of
c2,
c3;
let c5 be
SortSymbol of
c1;
func MSCng c4,
c5 -> Equivalence_Relation of the
Sorts of
a2 . a5 means :
Def19:
:: MSUALG_4:def 19
for
b1,
b2 being
Element of the
Sorts of
a2 . a5 holds
(
[b1,b2] in a6 iff
(a4 . a5) . b1 = (a4 . a5) . b2 );
existence
ex b1 being Equivalence_Relation of the Sorts of c2 . c5 st
for b2, b3 being Element of the Sorts of c2 . c5 holds
( [b2,b3] in b1 iff (c4 . c5) . b2 = (c4 . c5) . b3 )
uniqueness
for b1, b2 being Equivalence_Relation of the Sorts of c2 . c5 st ( for b3, b4 being Element of the Sorts of c2 . c5 holds
( [b3,b4] in b1 iff (c4 . c5) . b3 = (c4 . c5) . b4 ) ) & ( for b3, b4 being Element of the Sorts of c2 . c5 holds
( [b3,b4] in b2 iff (c4 . c5) . b3 = (c4 . c5) . b4 ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines MSCng MSUALG_4:def 19 :
:: deftheorem Def20 defines MSCng MSUALG_4:def 20 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2,
c3 be
non-empty MSAlgebra of
c1;
let c4 be
ManySortedFunction of
c2,
c3;
let c5 be
SortSymbol of
c1;
assume E17:
c4 is_homomorphism c2,
c3
;
func MSHomQuot c4,
c5 -> Function of the
Sorts of
(QuotMSAlg a2,(MSCng a4)) . a5,the
Sorts of
a3 . a5 means :
Def21:
:: MSUALG_4:def 21
for
b1 being
Element of the
Sorts of
a2 . a5 holds
a6 . (Class (MSCng a4,a5),b1) = (a4 . a5) . b1;
existence
ex b1 being Function of the Sorts of (QuotMSAlg c2,(MSCng c4)) . c5,the Sorts of c3 . c5 st
for b2 being Element of the Sorts of c2 . c5 holds b1 . (Class (MSCng c4,c5),b2) = (c4 . c5) . b2
uniqueness
for b1, b2 being Function of the Sorts of (QuotMSAlg c2,(MSCng c4)) . c5,the Sorts of c3 . c5 st ( for b3 being Element of the Sorts of c2 . c5 holds b1 . (Class (MSCng c4,c5),b3) = (c4 . c5) . b3 ) & ( for b3 being Element of the Sorts of c2 . c5 holds b2 . (Class (MSCng c4,c5),b3) = (c4 . c5) . b3 ) holds
b1 = b2
end;
:: deftheorem Def21 defines MSHomQuot MSUALG_4:def 21 :
definition
let c1 be non
empty non
void ManySortedSign ;
let c2,
c3 be
non-empty MSAlgebra of
c1;
let c4 be
ManySortedFunction of
c2,
c3;
func MSHomQuot c4 -> ManySortedFunction of
(QuotMSAlg a2,(MSCng a4)),
a3 means :
Def22:
:: MSUALG_4:def 22
for
b1 being
SortSymbol of
a1 holds
a5 . b1 = MSHomQuot a4,
b1;
existence
ex b1 being ManySortedFunction of (QuotMSAlg c2,(MSCng c4)),c3 st
for b2 being SortSymbol of c1 holds b1 . b2 = MSHomQuot c4,b2
uniqueness
for b1, b2 being ManySortedFunction of (QuotMSAlg c2,(MSCng c4)),c3 st ( for b3 being SortSymbol of c1 holds b1 . b3 = MSHomQuot c4,b3 ) & ( for b3 being SortSymbol of c1 holds b2 . b3 = MSHomQuot c4,b3 ) holds
b1 = b2
end;
:: deftheorem Def22 defines MSHomQuot MSUALG_4:def 22 :
theorem Th4: :: MSUALG_4:4
theorem Th5: :: MSUALG_4:5
theorem Th6: :: MSUALG_4:6