let S be locally_directed OrderSortedSign; :: thesis: 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 & OSNat_Hom U1,R is order-sorted )
let U1 be non-empty OSAlgebra of S; :: thesis: for R being OSCongruence of U1 holds
( OSNat_Hom U1,R is_epimorphism U1, QuotOSAlg U1,R & OSNat_Hom U1,R is order-sorted )
let R be OSCongruence of U1; :: thesis: ( OSNat_Hom U1,R is_epimorphism U1, QuotOSAlg U1,R & OSNat_Hom U1,R is order-sorted )
set F = OSNat_Hom U1,R;
set QA = QuotOSAlg U1,R;
set S1 = the Sorts of U1;
for o being Element of the carrier' of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds ((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x)
proof
let o be
Element of the
carrier' of
S;
:: thesis: ( Args o,U1 <> {} implies for x being Element of Args o,U1 holds ((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x) )
assume
Args o,
U1 <> {}
;
:: thesis: for x being Element of Args o,U1 holds ((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x)
let x be
Element of
Args o,
U1;
:: thesis: ((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x)
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
A1:
Den o,
(QuotOSAlg U1,R) =
(OSQuotCharact R) . o
by MSUALG_1:def 11
.=
OSQuotCharact R,
o
by Def21
;
A2:
(
dom ((OSNat_Hom U1,R) # x) = dom (the_arity_of o) &
dom x = dom (the_arity_of o) )
by MSUALG_3:6;
A3:
dom (R #_os x) = dom ((OSClass R) * (the_arity_of o))
by CARD_3:18;
dom (OSClass R) = the
carrier of
S
by PARTFUN1:def 4;
then
rng (the_arity_of o) c= dom (OSClass R)
;
then A4:
dom (R #_os x) = dom (the_arity_of o)
by A3, RELAT_1:46;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 6;
then A5:
(((OSClass R) # ) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o))
by MSAFREE:1;
for
a being
set st
a in dom (the_arity_of o) holds
((OSNat_Hom U1,R) # x) . a = (R #_os x) . a
proof
let a be
set ;
:: thesis: ( a in dom (the_arity_of o) implies ((OSNat_Hom U1,R) # x) . a = (R #_os x) . a )
assume A6:
a in dom (the_arity_of o)
;
:: thesis: ((OSNat_Hom U1,R) # x) . a = (R #_os x) . a
then reconsider n =
a as
Nat ;
set Fo =
OSNat_Hom U1,
R,
((the_arity_of o) /. n);
set s =
(the_arity_of o) /. n;
A7:
n in dom (the Sorts of U1 * (the_arity_of o))
by A6, PARTFUN1:def 4;
then (the Sorts of U1 * (the_arity_of o)) . n =
the
Sorts of
U1 . ((the_arity_of o) . n)
by FUNCT_1:22
.=
the
Sorts of
U1 . ((the_arity_of o) /. n)
by A6, PARTFUN1:def 8
;
then reconsider xn =
x . n as
Element of the
Sorts of
U1 . ((the_arity_of o) /. n) by A7, MSUALG_3:6;
consider z being
Element of the
Sorts of
U1 . ((the_arity_of o) /. n) such that A8:
(
z = x . n &
(R #_os x) . n = OSClass R,
z )
by A6, Def15;
thus ((OSNat_Hom U1,R) # x) . a =
((OSNat_Hom U1,R) . ((the_arity_of o) /. n)) . (x . n)
by A2, A6, MSUALG_3:def 8
.=
(OSNat_Hom U1,R,((the_arity_of o) /. n)) . xn
by Def24
.=
(R #_os x) . a
by A8, Def23
;
:: thesis: verum
end;
then A9:
(OSNat_Hom U1,R) # x = R #_os x
by A2, A4, FUNCT_1:9;
A10:
(
dom (Den o,U1) = Args o,
U1 &
rng (Den o,U1) c= Result o,
U1 )
by FUNCT_2:def 1;
A11:
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 4;
A12:
(
dom the
ResultSort of
S = the
carrier' of
S &
rng the
ResultSort of
S c= the
carrier of
S )
by FUNCT_2:def 1;
rng the
ResultSort of
S c= dom the
Sorts of
U1
by A11;
then
dom (the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by RELAT_1:46;
then A13:
(the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . (the ResultSort of S . o)
by A12, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
then A14:
Result o,
U1 = the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 10;
reconsider dx =
(Den o,U1) . x as
Element of the
Sorts of
U1 . (the_result_sort_of o) by A13, MSUALG_1:def 10;
rng (Den o,U1) c= dom (OSQuotRes R,o)
by A10, A13, A14, FUNCT_2:def 1;
then A15:
dom ((OSQuotRes R,o) * (Den o,U1)) = dom (Den o,U1)
by RELAT_1:46;
(Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x) =
((OSQuotRes R,o) * (Den o,U1)) . x
by A1, A5, A9, Def20
.=
(OSQuotRes R,o) . dx
by A10, A15, FUNCT_1:22
.=
OSClass R,
dx
by Def16
.=
(OSNat_Hom U1,R,(the_result_sort_of o)) . dx
by Def23
.=
((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x)
by Def24
;
hence
((OSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotOSAlg U1,R)) . ((OSNat_Hom U1,R) # x)
;
:: thesis: verum
end;
hence
OSNat_Hom U1,R is_homomorphism U1, QuotOSAlg U1,R
by MSUALG_3:def 9; :: according to MSUALG_3:def 10 :: thesis: ( OSNat_Hom U1,R is "onto" & OSNat_Hom U1,R is order-sorted )
for i being set st i in the carrier of S holds
rng ((OSNat_Hom U1,R) . i) = the Sorts of (QuotOSAlg U1,R) . i
proof
let i be
set ;
:: thesis: ( i in the carrier of S implies rng ((OSNat_Hom U1,R) . i) = the Sorts of (QuotOSAlg U1,R) . i )
assume
i in the
carrier of
S
;
:: thesis: rng ((OSNat_Hom U1,R) . i) = the Sorts of (QuotOSAlg U1,R) . i
then reconsider s =
i as
Element of
S ;
reconsider f =
(OSNat_Hom U1,R) . i as
Function of
(the Sorts of U1 . s),
(the Sorts of (QuotOSAlg U1,R) . s) by PBOOLE:def 18;
A16:
the
Sorts of
(QuotOSAlg U1,R) . s = OSClass R,
s
by Def13;
A17:
(
dom f = the
Sorts of
U1 . s &
rng f c= the
Sorts of
(QuotOSAlg U1,R) . s )
by FUNCT_2:def 1;
for
x being
set st
x in the
Sorts of
(QuotOSAlg U1,R) . i holds
x in rng f
proof
let x be
set ;
:: thesis: ( x in the Sorts of (QuotOSAlg U1,R) . i implies x in rng f )
assume
x in the
Sorts of
(QuotOSAlg U1,R) . i
;
:: thesis: x in rng f
then consider a1 being
set such that A18:
(
a1 in the
Sorts of
U1 . s &
x = Class (CompClass R,(CComp s)),
a1 )
by A16, Def12;
reconsider a2 =
a1 as
Element of the
Sorts of
U1 . s by A18;
A19:
OSClass R,
a2 = x
by A18;
A20:
f . a1 in rng f
by A17, A18, FUNCT_1:def 5;
f = OSNat_Hom U1,
R,
s
by Def24;
hence
x in rng f
by A19, A20, Def23;
:: thesis: verum
end;
then
the
Sorts of
(QuotOSAlg U1,R) . i c= rng f
by TARSKI:def 3;
hence
rng ((OSNat_Hom U1,R) . i) = the
Sorts of
(QuotOSAlg U1,R) . i
by XBOOLE_0:def 10;
:: thesis: verum
end;
hence
OSNat_Hom U1,R is "onto"
by MSUALG_3:def 3; :: thesis: OSNat_Hom U1,R is order-sorted
thus
OSNat_Hom U1,R is order-sorted
:: thesis: verumproof
let s1,
s2 be
Element of
S;
:: according to OSALG_3:def 1 :: thesis: ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSNat_Hom U1,R) . s1) or ( b1 in dom ((OSNat_Hom U1,R) . s2) & ((OSNat_Hom U1,R) . s1) . b1 = ((OSNat_Hom U1,R) . s2) . b1 ) ) )
assume A21:
s1 <= s2
;
:: thesis: for b1 being set holds
( not b1 in dom ((OSNat_Hom U1,R) . s1) or ( b1 in dom ((OSNat_Hom U1,R) . s2) & ((OSNat_Hom U1,R) . s1) . b1 = ((OSNat_Hom U1,R) . s2) . b1 ) )
let a1 be
set ;
:: thesis: ( not a1 in dom ((OSNat_Hom U1,R) . s1) or ( a1 in dom ((OSNat_Hom U1,R) . s2) & ((OSNat_Hom U1,R) . s1) . a1 = ((OSNat_Hom U1,R) . s2) . a1 ) )
assume A22:
a1 in dom ((OSNat_Hom U1,R) . s1)
;
:: thesis: ( a1 in dom ((OSNat_Hom U1,R) . s2) & ((OSNat_Hom U1,R) . s1) . a1 = ((OSNat_Hom U1,R) . s2) . a1 )
reconsider S2 = the
Sorts of
U1 as
OrderSortedSet of
by OSALG_1:17;
A23:
S2 . s1 c= S2 . s2
by A21, OSALG_1:def 18;
A24:
dom ((OSNat_Hom U1,R) . s2) = the
Sorts of
U1 . s2
by FUNCT_2:def 1;
A25:
a1 in the
Sorts of
U1 . s1
by A22;
hence
a1 in dom ((OSNat_Hom U1,R) . s2)
by A23, A24;
:: thesis: ((OSNat_Hom U1,R) . s1) . a1 = ((OSNat_Hom U1,R) . s2) . a1
reconsider b1 =
a1 as
Element of the
Sorts of
U1 . s1 by A22;
reconsider b2 =
a1 as
Element of the
Sorts of
U1 . s2 by A23, A25;
thus ((OSNat_Hom U1,R) . s1) . a1 =
(OSNat_Hom U1,R,s1) . b1
by Def24
.=
OSClass R,
b1
by Def23
.=
OSClass R,
b2
by A21, Th5
.=
(OSNat_Hom U1,R,s2) . b2
by Def23
.=
((OSNat_Hom U1,R) . s2) . a1
by Def24
;
:: thesis: verum
end;