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