:: Order Sorted Quotient Algebra
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

registration
let R be non empty Poset;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding order-sorted for set ;
existence
 ex b1 being OrderSortedSet of R st b1 is Relation-yielding
proofend;
end;

:: this is a stronger condition for relation than just being order-sorted
definition
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attrIT is os-compatible  means :Def1: :: OSALG_4:def 1
 for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 &amp; y in B . s1 holds
( [x,y] in IT . s1 iff [x,y] in IT . s2 );
end;

:: deftheorem Def1 defines os-compatible OSALG_4:def_1_:_
 for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for IT being ManySortedRelation of A,B holds
( IT is os-compatible iff for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 &amp; y in B . s1 holds
( [x,y] in IT . s1 iff [x,y] in IT . s2 ) );

registration
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding os-compatible for ManySortedRelation of A,B;
existence
 ex b1 being ManySortedRelation of A,B st b1 is os-compatible
proofend;
end;

definition
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;
end;

theorem Th1: :: OSALG_4:1
for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R
proofend;

registration
let R be non empty Poset;
let A, B be ManySortedSet of R;
cluster os-compatible  ->  order-sorted for ManySortedRelation of A,B;
coherence
 for b1 being ManySortedRelation of A,B st b1 is os-compatible holds
b1 is order-sorted by Th1;
end;

definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A is OrderSortedRelation of A,A;
end;

definition
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
mode OrderSortedRelation of U1 ->  ManySortedRelation of U1 means :Def2: :: OSALG_4:def 2
it is os-compatible ;
existence
 ex b1 being ManySortedRelation of U1 st b1 is os-compatible
proofend;
end;

:: deftheorem Def2 defines OrderSortedRelation OSALG_4:def_2_:_
 for S being OrderSortedSign
for U1 being OSAlgebra of S
for b3 being ManySortedRelation of U1 holds
( b3 is OrderSortedRelation of U1 iff b3 is os-compatible );

:: REVISE: the definition of ManySorted diagonal from MSUALG_6
:: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6
:: should replace the MSCongruence-like
registration
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for OrderSortedRelation of U1;
existence
 ex b1 being OrderSortedRelation of U1 st b1 is MSEquivalence-like
proofend;
end;

:: REVISE: we need the fact that id has the type,
:: the original prf can be simplified
registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;
existence
 ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is MSCongruence-like
proofend;
end;

definition
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
end;

:: TODO: a smooth transition between Relations and Graphs would
:: be useful here, the FinSequence approach seemed to me faster than
:: transitive closure of R \/ R" .. maybe not, can be later a theorem
:: all could be done generally for reflexive (or with small
:: modification even non reflexive) Relations
:: I found ex post that attributes disconnected and connected defined
:: in ORDERS_3 have st. in common here, but the theory there is not developed
:: suggested improvements: f connects x,y; x is_connected_with y;
:: connected iff for x,y holds x is_connected_with y
:: finally I found this is the EqCl from MSUALG_5 - should be merged
definition
let R be non empty Poset;
func Path_Rel R ->  Equivalence_Relation of the carrier of R means :Def3: :: OSALG_4:def 3
 for x, y being set holds
( [x,y] in it iff ( x in the carrier of R &amp; y in the carrier of R &amp; ex p being FinSequence of the carrier of R st
( 1 < len p &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for n being Nat st 2 <= n &amp; n <= len p &amp; not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) );
existence
 ex b1 being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of R &amp; y in the carrier of R &amp; ex p being FinSequence of the carrier of R st
( 1 < len p &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for n being Nat st 2 <= n &amp; n <= len p &amp; not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of the carrier of R st ( for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of R &amp; y in the carrier of R &amp; ex p being FinSequence of the carrier of R st
( 1 < len p &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for n being Nat st 2 <= n &amp; n <= len p &amp; not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) &amp; ( for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of R &amp; y in the carrier of R &amp; ex p being FinSequence of the carrier of R st
( 1 < len p &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for n being Nat st 2 <= n &amp; n <= len p &amp; not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Path_Rel OSALG_4:def_3_:_
 for R being non empty Poset
for b2 being Equivalence_Relation of the carrier of R holds
( b2 = Path_Rel R iff for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of R &amp; y in the carrier of R &amp; ex p being FinSequence of the carrier of R st
( 1 < len p &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for n being Nat st 2 <= n &amp; n <= len p &amp; not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) );

theorem Th2: :: OSALG_4:2
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
proofend;

:: again, should be defined for Relations probably
definition
let R be non empty Poset;
let s1, s2 be Element of R;
preds1 ~= s2 means :Def4: :: OSALG_4:def 4
[s1,s2] in Path_Rel R;
reflexivity
 for s1 being Element of R holds [s1,s1] in Path_Rel R
proofend;
symmetry
 for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds
[s2,s1] in Path_Rel R
proofend;
end;

:: deftheorem Def4 defines ~= OSALG_4:def_4_:_
 for R being non empty Poset
for s1, s2 being Element of R holds
( s1 ~= s2 iff [s1,s2] in Path_Rel R );

theorem :: OSALG_4:3
for R being non empty Poset
for s1, s2, s3 being Element of R st s1 ~= s2 &amp; s2 ~= s3 holds
s1 ~= s3
proofend;

:: do for Relations
definition
let R be non empty Poset;
func Components R ->  non empty Subset-Family of R equals :: OSALG_4:def 5
 Class (Path_Rel R);
coherence
 Class (Path_Rel R) is non empty Subset-Family of R ;
end;

:: deftheorem  defines Components OSALG_4:def_5_:_
 for R being non empty Poset holds Components R = Class (Path_Rel R);

registration
let R be non empty Poset;
cluster  ->  non empty for Element of Components R;
coherence
 for b1 being Element of Components R holds not b1 is empty
proofend;
end;

definition
let R be non empty Poset;
mode Component of R is Element of Components R;
end;

definition
let R be non empty Poset;
let s1 be Element of R;
func CComp s1 ->  Component of R equals :: OSALG_4:def 6
 Class ((Path_Rel R),s1);
correctness
coherence
Class ((Path_Rel R),s1) is Component of R;
by EQREL_1:def_3;
end;

:: deftheorem  defines CComp OSALG_4:def_6_:_
 for R being non empty Poset
for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1);

theorem Th4: :: OSALG_4:4
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2
proofend;

definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
let C be Component of R;
funcA -carrier_of C ->  set  equals :: OSALG_4:def 7
 union  {  (A . s) where s is Element of R : s in C  }  ;
correctness
coherence
union  {  (A . s) where s is Element of R : s in C  }  is set ;
;
end;

:: deftheorem  defines -carrier_of OSALG_4:def_7_:_
 for R being non empty Poset
for A being ManySortedSet of the carrier of R
for C being Component of R holds A -carrier_of C = union  {  (A . s) where s is Element of R : s in C  }  ;

theorem Th5: :: OSALG_4:5
for R being non empty Poset
for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
proofend;

definition
let R be non empty Poset;
attrR is locally_directed  means :Def8: :: OSALG_4:def 8
 for C being Component of R holds C is directed ;
end;

:: deftheorem Def8 defines locally_directed OSALG_4:def_8_:_
 for R being non empty Poset holds
( R is locally_directed iff for C being Component of R holds C is directed );

theorem Th6: :: OSALG_4:6
for R being non empty discrete Poset
for x, y being Element of R st [x,y] in Path_Rel R holds
x = y
proofend;

theorem Th7: :: OSALG_4:7
for R being non empty discrete Poset
for C being Component of R ex x being Element of R st C = {x}
proofend;

theorem Th8: :: OSALG_4:8
for R being non empty discrete Poset holds R is locally_directed
proofend;

:: the system could generate this one from the following
registration
cluster non empty reflexive transitive antisymmetric locally_directed for RelStr ;
existence
 ex b1 being non empty Poset st b1 is locally_directed
proofend;
end;

registration
cluster non empty non void V73() reflexive transitive antisymmetric order-sorted discernable locally_directed for OverloadedRSSign ;
existence
 ex b1 being OrderSortedSign st b1 is locally_directed
proofend;
end;

registration
cluster non empty reflexive transitive antisymmetric discrete  ->  non empty locally_directed for RelStr ;
coherence
 for b1 being non empty Poset st b1 is discrete holds
b1 is locally_directed by Th8;
end;

registration
let S be non empty locally_directed Poset;
cluster  ->  directed for Element of Components S;
coherence
 for b1 being Component of S holds b1 is directed by Def8;
end;

theorem Th9: :: OSALG_4:9
{} is Equivalence_Relation of {} by RELSET_1:12;

:: Much of what follows can be done generally for OrderSortedRelations
:: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras),
:: unfortunately, multiple inheritence would be needed to widen the
:: latter to the former
:: Classes on connected components
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let C be Component of S;
func CompClass (E,C) ->  Equivalence_Relation of ( the Sorts of A -carrier_of C) means :Def9: :: OSALG_4:def 9
 for x, y being set holds
( [x,y] in it iff ex s1 being Element of S st
( s1 in C &amp; [x,y] in E . s1 ) );
existence
 ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C &amp; [x,y] in E . s1 ) )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st ( for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C &amp; [x,y] in E . s1 ) ) ) &amp; ( for x, y being set holds
( [x,y] in b2 iff ex s1 being Element of S st
( s1 in C &amp; [x,y] in E . s1 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines CompClass OSALG_4:def_9_:_
 for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for C being Component of S
for b5 being Equivalence_Relation of ( the Sorts of A -carrier_of C) holds
( b5 = CompClass (E,C) iff for x, y being set holds
( [x,y] in b5 iff ex s1 being Element of S st
( s1 in C &amp; [x,y] in E . s1 ) ) );

:: we could give a name to Class CompClass(E,C)
:: restriction of Class CompClass(E,C) to A.s1
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
func OSClass (E,s1) ->  Subset of (Class (CompClass (E,(CComp s1)))) means :Def10: :: OSALG_4:def 10
 for z being set holds
( z in it iff ex x being set st
( x in the Sorts of A . s1 &amp; z = Class ((CompClass (E,(CComp s1))),x) ) );
existence
 ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st
for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 &amp; z = Class ((CompClass (E,(CComp s1))),x) ) )
proofend;
uniqueness
 for b1, b2 being Subset of (Class (CompClass (E,(CComp s1)))) st ( for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 &amp; z = Class ((CompClass (E,(CComp s1))),x) ) ) ) &amp; ( for z being set holds
( z in b2 iff ex x being set st
( x in the Sorts of A . s1 &amp; z = Class ((CompClass (E,(CComp s1))),x) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines OSClass OSALG_4:def_10_:_
 for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1 being Element of S
for b5 being Subset of (Class (CompClass (E,(CComp s1)))) holds
( b5 = OSClass (E,s1) iff for z being set holds
( z in b5 iff ex x being set st
( x in the Sorts of A . s1 &amp; z = Class ((CompClass (E,(CComp s1))),x) ) ) );

registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
cluster OSClass (E,s1) ->  non empty ;
coherence
 not OSClass (E,s1) is empty
proofend;
end;

theorem Th10: :: OSALG_4:10
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1, s2 being Element of S st s1 <= s2 holds
OSClass (E,s1) c= OSClass (E,s2)
proofend;

:: finally, this is analogy of the Many-Sorted Class E for order-sorted E
:: this definition should work for order-sorted MSCongruence too
:: if non-empty not needed, prove the following cluster
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E ->  OrderSortedSet of S means :Def11: :: OSALG_4:def 11
 for s1 being Element of S holds it . s1 = OSClass (E,s1);
existence
 ex b1 being OrderSortedSet of S st
for s1 being Element of S holds b1 . s1 = OSClass (E,s1)
proofend;
uniqueness
 for b1, b2 being OrderSortedSet of S st ( for s1 being Element of S holds b1 . s1 = OSClass (E,s1) ) &amp; ( for s1 being Element of S holds b2 . s1 = OSClass (E,s1) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines OSClass OSALG_4:def_11_:_
 for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for b4 being OrderSortedSet of S holds
( b4 = OSClass E iff for s1 being Element of S holds b4 . s1 = OSClass (E,s1) );

registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> V17() ;
coherence
 OSClass E is non-empty
proofend;
end;

:: order-sorted equiv of Class(R,x)
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x be Element of the Sorts of U1 . s;
func OSClass (E,x) ->  Element of OSClass (E,s) equals :: OSALG_4:def 12
 Class ((CompClass (E,(CComp s))),x);
correctness
coherence
Class ((CompClass (E,(CComp s))),x) is Element of OSClass (E,s);
by Def10;
end;

:: deftheorem  defines OSClass OSALG_4:def_12_:_
 for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x);

theorem :: OSALG_4:11
for R being non empty locally_directed Poset
for x, y being Element of R st ex z being Element of R st
( z <= x &amp; z <= y ) holds
ex u being Element of R st
( x <= u &amp; y <= u )
proofend;

theorem Th12: :: OSALG_4:12
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )
proofend;

theorem :: OSALG_4:13
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s1, s2 being Element of S
for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds
for y being Element of the Sorts of U1 . s2 st y = x holds
OSClass (E,x) = OSClass (E,y) by Th4;

begin

:: multiclasses
definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
let x be Element of Args (o,A);
funcR #_os x ->  Element of product ((OSClass R) * (the_arity_of o)) means :Def13: :: OSALG_4:def 13
 for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n &amp; it . n = OSClass (R,y) );
existence
 ex b1 being Element of product ((OSClass R) * (the_arity_of o)) st
for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n &amp; b1 . n = OSClass (R,y) )
proofend;
uniqueness
 for b1, b2 being Element of product ((OSClass R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n &amp; b1 . n = OSClass (R,y) ) ) &amp; ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n &amp; b2 . n = OSClass (R,y) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines #_os OSALG_4:def_13_:_
 for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being Element of Args (o,A)
for b6 being Element of product ((OSClass R) * (the_arity_of o)) holds
( b6 = R #_os x iff for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n &amp; b6 . n = OSClass (R,y) ) );

:: the quotient will be different for order-sorted;
:: this def seems ok for order-sorted
definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes (R,o) ->  Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def14: :: OSALG_4:def 14
 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x);
existence
 ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st
for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x)
proofend;
uniqueness
 for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x) ) &amp; ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = OSClass (R,x) ) holds
b1 = b2
proofend;
func OSQuotArgs (R,o) ->  Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) means :: OSALG_4:def 15
 for x being Element of Args (o,A) holds it . x = R #_os x;
existence
 ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st
for x being Element of Args (o,A) holds b1 . x = R #_os x
proofend;
uniqueness
 for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R #_os x ) &amp; ( for x being Element of Args (o,A) holds b2 . x = R #_os x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines OSQuotRes OSALG_4:def_14_:_
 for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b5 = OSQuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = OSClass (R,x) );

:: deftheorem  defines OSQuotArgs OSALG_4:def_15_:_
 for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) holds
( b5 = OSQuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R #_os x );

definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes R ->  ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S means :: OSALG_4:def 16
 for o being OperSymbol of S holds it . o = OSQuotRes (R,o);
existence
 ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o) ) &amp; ( for o being OperSymbol of S holds b2 . o = OSQuotRes (R,o) ) holds
b1 = b2
proofend;
func OSQuotArgs R ->  ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S means :: OSALG_4:def 17
 for o being OperSymbol of S holds it . o = OSQuotArgs (R,o);
existence
 ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st
for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o) ) &amp; ( for o being OperSymbol of S holds b2 . o = OSQuotArgs (R,o) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines OSQuotRes OSALG_4:def_16_:_
 for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotRes R iff for o being OperSymbol of S holds b4 . o = OSQuotRes (R,o) );

:: deftheorem  defines OSQuotArgs OSALG_4:def_17_:_
 for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S holds
( b4 = OSQuotArgs R iff for o being OperSymbol of S holds b4 . o = OSQuotArgs (R,o) );

theorem Th14: :: OSALG_4:14
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
proofend;

definition
let S be locally_directed OrderSortedSign;
let o be Element of the carrier' of S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact (R,o) ->  Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def18: :: OSALG_4:def 18
 for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
it . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a;
existence
 ex b1 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st
for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a
proofend;
uniqueness
 for b1, b2 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) &amp; ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b2 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines OSQuotCharact OSALG_4:def_18_:_
 for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b5 = OSQuotCharact (R,o) iff for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b5 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a );

definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact R ->  ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S means :Def19: :: OSALG_4:def 19
 for o being OperSymbol of S holds it . o = OSQuotCharact (R,o);
existence
 ex b1 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o) ) &amp; ( for o being OperSymbol of S holds b2 . o = OSQuotCharact (R,o) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines OSQuotCharact OSALG_4:def_19_:_
 for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotCharact R iff for o being OperSymbol of S holds b4 . o = OSQuotCharact (R,o) );

definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func QuotOSAlg (U1,R) ->  OSAlgebra of S equals :: OSALG_4:def 20
 MSAlgebra(# (OSClass R),(OSQuotCharact R) #);
coherence
 MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S by OSALG_1:17;
end;

:: deftheorem  defines QuotOSAlg OSALG_4:def_20_:_
 for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #);

:: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal
registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg (U1,R) ->  strict non-empty ;
coherence
 ( QuotOSAlg (U1,R) is strict &amp; QuotOSAlg (U1,R) is non-empty ) by MSUALG_1:def_3;
end;

definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
let s be Element of S;
func OSNat_Hom (U1,R,s) ->  Function of ( the Sorts of U1 . s),(OSClass (R,s)) means :Def21: :: OSALG_4:def 21
 for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x);
existence
 ex b1 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st
for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x)
proofend;
uniqueness
 for b1, b2 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st ( for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x) ) &amp; ( for x being Element of the Sorts of U1 . s holds b2 . x = OSClass (R,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines OSNat_Hom OSALG_4:def_21_:_
 for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for s being Element of S
for b5 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) holds
( b5 = OSNat_Hom (U1,R,s) iff for x being Element of the Sorts of U1 . s holds b5 . x = OSClass (R,x) );

definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func OSNat_Hom (U1,R) ->  ManySortedFunction of U1,(QuotOSAlg (U1,R)) means :Def22: :: OSALG_4:def 22
 for s being Element of S holds it . s = OSNat_Hom (U1,R,s);
existence
 ex b1 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st
for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st ( for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s) ) &amp; ( for s being Element of S holds b2 . s = OSNat_Hom (U1,R,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines OSNat_Hom OSALG_4:def_22_:_
 for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) holds
( b4 = OSNat_Hom (U1,R) iff for s being Element of S holds b4 . s = OSNat_Hom (U1,R,s) );

theorem :: OSALG_4:15
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) &amp; OSNat_Hom (U1,R) is order-sorted )
proofend;

theorem Th16: :: OSALG_4:16
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 &amp; F is order-sorted holds
MSCng F is OSCongruence of U1
proofend;

:: just a casting func, currently no other way how to employ the type system
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume A1: ( F is_homomorphism U1,U2 &amp; F is order-sorted ) ;
func OSCng F ->  OSCongruence of U1 equals :Def23: :: OSALG_4:def 23
 MSCng F;
correctness
coherence
MSCng F is OSCongruence of U1;
by A1, Th16;
end;

:: deftheorem Def23 defines OSCng OSALG_4:def_23_:_
 for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 &amp; F is order-sorted holds
OSCng F = MSCng F;

definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ;
func OSHomQuot (F,s) ->  Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) means :Def24: :: OSALG_4:def 24
 for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x;
existence
 ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x
proofend;
uniqueness
 for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x ) &amp; ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass ((OSCng F),x)) = (F . s) . x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def24 defines OSHomQuot OSALG_4:def_24_:_
 for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for s being Element of S st F is_homomorphism U1,U2 &amp; F is order-sorted holds
for b6 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) holds
( b6 = OSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (OSClass ((OSCng F),x)) = (F . s) . x );

:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
func OSHomQuot F ->  ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 means :Def25: :: OSALG_4:def 25
 for s being Element of S holds it . s = OSHomQuot (F,s);
existence
 ex b1 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,s)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,s) ) &amp; ( for s being Element of S holds b2 . s = OSHomQuot (F,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines OSHomQuot OSALG_4:def_25_:_
 for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for b5 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 holds
( b5 = OSHomQuot F iff for s being Element of S holds b5 . s = OSHomQuot (F,s) );

theorem Th17: :: OSALG_4:17
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 &amp; F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 &amp; OSHomQuot F is order-sorted )
proofend;

theorem Th18: :: OSALG_4:18
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 &amp; F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
proofend;

theorem :: OSALG_4:19
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 &amp; F is order-sorted holds
QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
proofend;

:: monotone OSCongruence ... monotonicity is properly stronger
:: than MSCongruence, so we define it more broadly and prove the
:: ccluster then, however if used for other things than OSCongruences
:: the name of the attribute should be changed
:: this condition is nontrivial only for nonmonotone osas (see further),
:: where Den(o1,U1).x1 can differ from Den(o2,U2).x1
:: is OK for constants ... their Args is always {{}}, so o1 <= o2
:: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R
definition
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be MSEquivalence-like OrderSortedRelation of U1;
attrR is monotone  means :Def26: :: OSALG_4:def 26
 for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2);
end;

:: deftheorem Def26 defines monotone OSALG_4:def_26_:_
 for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like OrderSortedRelation of U1 holds
( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) );

theorem Th20: :: OSALG_4:20
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1
proofend;

theorem Th21: :: OSALG_4:21
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone
proofend;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like monotone for OrderSortedRelation of U1;
existence
 ex b1 being OSCongruence of U1 st b1 is monotone
proofend;
end;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like monotone for OrderSortedRelation of U1;
existence
 ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone
proofend;
end;

theorem Th22: :: OSALG_4:22
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
proofend;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like monotone  ->  MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;
coherence
 for b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone holds
b1 is MSCongruence-like by Th22;
end;

theorem Th23: :: OSALG_4:23
for S being OrderSortedSign
for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone
proofend;

registration
let S be OrderSortedSign;
let U1 be non-empty monotone OSAlgebra of S;
cluster MSEquivalence-like MSCongruence-like  ->  monotone for OrderSortedRelation of U1;
coherence
 for b1 being OSCongruence of U1 holds b1 is monotone by Th23;
end;

:: monotonicity of quotient by monotone oscongruence
registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg (U1,R) ->  monotone ;
coherence
 QuotOSAlg (U1,R) is monotone
proofend;
end;

theorem :: OSALG_4:24
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 &amp; F is order-sorted holds
OSCng F is monotone
proofend;

:: these are a bit more general versions of OSHomQuot, that
:: I need for OSAFREE; more proper way how to do this is restating
:: the MSUALG_9 quotient theorems for OSAs, but that's more work
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
let s be Element of S;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted and
A3: R c= OSCng F ;
func OSHomQuot (F,R,s) ->  Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) means :Def27: :: OSALG_4:def 27
 for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x;
existence
 ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x
proofend;
uniqueness
 for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x ) &amp; ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass (R,x)) = (F . s) . x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def27 defines OSHomQuot OSALG_4:def_27_:_
 for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1
for s being Element of S st F is_homomorphism U1,U2 &amp; F is order-sorted &amp; R c= OSCng F holds
for b7 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) holds
( b7 = OSHomQuot (F,R,s) iff for x being Element of the Sorts of U1 . s holds b7 . (OSClass (R,x)) = (F . s) . x );

:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition
let S be locally_directed OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
func OSHomQuot (F,R) ->  ManySortedFunction of (QuotOSAlg (U1,R)),U2 means :Def28: :: OSALG_4:def 28
 for s being Element of S holds it . s = OSHomQuot (F,R,s);
existence
 ex b1 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,R,s)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,R,s) ) &amp; ( for s being Element of S holds b2 . s = OSHomQuot (F,R,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def28 defines OSHomQuot OSALG_4:def_28_:_
 for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1
for b6 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 holds
( b6 = OSHomQuot (F,R) iff for s being Element of S holds b6 . s = OSHomQuot (F,R,s) );

theorem :: OSALG_4:25
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 &amp; F is order-sorted &amp; R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 &amp; OSHomQuot (F,R) is order-sorted )
proofend;