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 9;
then consider a being
Element of
Args o,
U1 such that A5:
x = R #_os a
by Th15;
A6:
dom a = dom (the_arity_of o)
by MSUALG_3:6;
A7:
now let y be
set ;
( 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 5;
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 8;
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, Def15;
((OSHomQuot F,R) # x) . n =
((OSHomQuot F,R) . s) . (x . n)
by A4, A8, A9, MSUALG_3:def 8
.=
(OSHomQuot F,R,s) . (OSClass R,an)
by A11, Def30
.=
(F . s) . an
by A1, A2, A3, Def29
.=
(F # a) . n
by A6, A8, A9, A10, MSUALG_3:def 8
;
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 4;
then A12:
(the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . (the ResultSort of S . o)
by FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
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 10;
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:46;
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 6;
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 10;
A15:
(OSHomQuot F,R) . (the_result_sort_of o) = OSHomQuot F,
R,
(the_result_sort_of o)
by Def30;
Den o,
(QuotOSAlg U1,R) =
(OSQuotCharact R) . o
by MSUALG_1:def 11
.=
OSQuotCharact R,
o1
by Def21
;
then (Den o,(QuotOSAlg U1,R)) . x =
((OSQuotRes R,o) * (Den o,U1)) . a
by A5, A14, Def20
.=
(OSQuotRes R,o) . da
by A13, FUNCT_1:22
.=
OSClass R,
da
by Def16
;
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, Def29
.=
(Den o,U2) . (F # a)
by A1, MSUALG_3:def 9
;
(
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:9;
verum
end;
hence
OSHomQuot F,R is_homomorphism QuotOSAlg U1,R,U2
by MSUALG_3:def 9; 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 proj1 ((OSHomQuot F,R) . s1) or ( b1 in proj1 ((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 proj1 ((OSHomQuot F,R) . s1) or ( b1 in proj1 ((OSHomQuot F,R) . s2) & ((OSHomQuot F,R) . s1) . b1 = ((OSHomQuot F,R) . s2) . b1 ) )
let a1 be
set ;
( not a1 in proj1 ((OSHomQuot F,R) . s1) or ( a1 in proj1 ((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 proj1 ((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 Def13;
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 Def12;
S1O . s1 c= S1O . s2
by A17, OSALG_1:def 18;
then reconsider x2 =
x as
Element of the
Sorts of
U1 . s2 by A19;
A21:
a1 = OSClass R,
x2
by A17, A20, Th5;
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, OSALG_3:def 1;
sqa . s1 c= sqa . s2
by A17, OSALG_1:def 18;
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, Def30
.=
(F . s2) . x1
by A1, A2, A3, A23, Def29
.=
(OSHomQuot F,R,s2) . (OSClass R,x2)
by A1, A2, A3, Def29
.=
((OSHomQuot F,R) . s2) . a1
by A21, Def30
;
verum
end;