let S be 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 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let U1, U2 be non-empty OSAlgebra of S; for F being ManySortedFunction of U1,U2
for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let F be ManySortedFunction of U1,U2; for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds
( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
let R be OSCongruence of U1; ( F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F implies ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted ) )
set mc = R;
set qa = QuotOSAlg (U1,R);
set qh = OSHomQuot (F,R);
set S1 = the Sorts of U1;
assume that
A1:
F is_homomorphism U1,U2
and
A2:
F is order-sorted
and
A3:
R c= OSCng F
; ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )
for o being Element of the carrier' of S st Args (o,(QuotOSAlg (U1,R))) <> {} holds
for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
proof
let o be
Element of the
carrier' of
S;
( Args (o,(QuotOSAlg (U1,R))) <> {} implies for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) )
assume
Args (
o,
(QuotOSAlg (U1,R)))
<> {}
;
for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
let x be
Element of
Args (
o,
(QuotOSAlg (U1,R)));
((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
reconsider o1 =
o as
OperSymbol of
S ;
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
A4:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
Args (
o,
(QuotOSAlg (U1,R)))
= (((OSClass R) #) * the Arity of S) . o
by MSUALG_1:def 4;
then consider a being
Element of
Args (
o,
U1)
such that A5:
x = R #_os a
by Th14;
A6:
dom a = dom (the_arity_of o)
by MSUALG_3:6;
A7:
now for y being object st y in dom (the_arity_of o) holds
((OSHomQuot (F,R)) # x) . y = (F # a) . ylet y be
object ;
( y in dom (the_arity_of o) implies ((OSHomQuot (F,R)) # x) . y = (F # a) . y )assume A8:
y in dom (the_arity_of o)
;
((OSHomQuot (F,R)) # x) . y = (F # a) . ythen reconsider n =
y as
Nat ;
(the_arity_of o) . n in rng (the_arity_of o)
by A8, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . n as
SortSymbol of
S ;
A9:
(the_arity_of o) /. n = (the_arity_of o) . n
by A8, PARTFUN1:def 6;
then consider an being
Element of the
Sorts of
U1 . s such that A10:
an = a . n
and A11:
x . n = OSClass (
R,
an)
by A5, A8, Def13;
((OSHomQuot (F,R)) # x) . n =
((OSHomQuot (F,R)) . s) . (x . n)
by A4, A8, A9, MSUALG_3:def 6
.=
(OSHomQuot (F,R,s)) . (OSClass (R,an))
by A11, Def28
.=
(F . s) . an
by A1, A2, A3, Def27
.=
(F # a) . n
by A6, A8, A9, A10, MSUALG_3:def 6
;
hence
((OSHomQuot (F,R)) # x) . y = (F # a) . y
;
verum end;
o in the
carrier' of
S
;
then
o in dom ( the Sorts of U1 * the ResultSort of S)
by PARTFUN1:def 2;
then A12:
( the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . ( the ResultSort of S . o)
by FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 2
;
then
(
rng (Den (o,U1)) c= Result (
o,
U1) &
Result (
o,
U1)
= the
Sorts of
U1 . (the_result_sort_of o) )
by MSUALG_1:def 5;
then
rng (Den (o,U1)) c= dom (OSQuotRes (R,o))
by A12, FUNCT_2:def 1;
then A13:
(
dom (Den (o,U1)) = Args (
o,
U1) &
dom ((OSQuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) )
by FUNCT_2:def 1, RELAT_1:27;
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 1;
then A14:
product ((OSClass R) * (the_arity_of o)) = (((OSClass R) #) * the Arity of S) . o
by MSAFREE:1;
reconsider da =
(Den (o,U1)) . a as
Element of the
Sorts of
U1 . (the_result_sort_of o) by A12, MSUALG_1:def 5;
A15:
(OSHomQuot (F,R)) . (the_result_sort_of o) = OSHomQuot (
F,
R,
(the_result_sort_of o))
by Def28;
Den (
o,
(QuotOSAlg (U1,R))) =
(OSQuotCharact R) . o
by MSUALG_1:def 6
.=
OSQuotCharact (
R,
o1)
by Def19
;
then (Den (o,(QuotOSAlg (U1,R)))) . x =
((OSQuotRes (R,o)) * (Den (o,U1))) . a
by A5, A14, Def18
.=
(OSQuotRes (R,o)) . da
by A13, FUNCT_1:12
.=
OSClass (
R,
da)
by Def14
;
then A16:
((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) =
(F . (the_result_sort_of o)) . ((Den (o,U1)) . a)
by A1, A2, A3, A15, Def27
.=
(Den (o,U2)) . (F # a)
by A1
;
(
dom ((OSHomQuot (F,R)) # x) = dom (the_arity_of o) &
dom (F # a) = dom (the_arity_of o) )
by MSUALG_3:6;
hence
((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x)
by A7, A16, FUNCT_1:2;
verum
end;
hence
OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2
; OSHomQuot (F,R) is order-sorted
thus
OSHomQuot (F,R) is order-sorted
verumproof
reconsider S1O = the
Sorts of
U1 as
OrderSortedSet of
S by OSALG_1:17;
reconsider sqa = the
Sorts of
(QuotOSAlg (U1,R)) as
OrderSortedSet of
S ;
let s1,
s2 be
Element of
S;
OSALG_3:def 1 ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) ) )
assume A17:
s1 <= s2
;
for b1 being set holds
( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) )
let a1 be
set ;
( not a1 in dom ((OSHomQuot (F,R)) . s1) or ( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 ) )
assume A18:
a1 in dom ((OSHomQuot (F,R)) . s1)
;
( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 )
a1 in (OSClass R) . s1
by A18;
then
a1 in OSClass (
R,
s1)
by Def11;
then consider x being
set such that A19:
x in the
Sorts of
U1 . s1
and A20:
a1 = Class (
(CompClass (R,(CComp s1))),
x)
by Def10;
S1O . s1 c= S1O . s2
by A17, OSALG_1:def 16;
then reconsider x2 =
x as
Element of the
Sorts of
U1 . s2 by A19;
A21:
a1 = OSClass (
R,
x2)
by A17, A20, Th4;
reconsider s3 =
s1,
s4 =
s2 as
Element of
S ;
A22:
(
dom ((OSHomQuot (F,R)) . s1) = the
Sorts of
(QuotOSAlg (U1,R)) . s1 &
dom ((OSHomQuot (F,R)) . s2) = the
Sorts of
(QuotOSAlg (U1,R)) . s2 )
by FUNCT_2:def 1;
reconsider x1 =
x as
Element of the
Sorts of
U1 . s1 by A19;
x1 in dom (F . s3)
by A19, FUNCT_2:def 1;
then A23:
(F . s3) . x1 = (F . s4) . x1
by A2, A17;
sqa . s1 c= sqa . s2
by A17, OSALG_1:def 16;
hence
a1 in dom ((OSHomQuot (F,R)) . s2)
by A18, A22;
((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1
thus ((OSHomQuot (F,R)) . s1) . a1 =
(OSHomQuot (F,R,s1)) . (OSClass (R,x1))
by A20, Def28
.=
(F . s2) . x1
by A1, A2, A3, A23, Def27
.=
(OSHomQuot (F,R,s2)) . (OSClass (R,x2))
by A1, A2, A3, Def27
.=
((OSHomQuot (F,R)) . s2) . a1
by A21, Def28
;
verum
end;