reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set A = QuotOSAlg (U1,R);
let o1, o2 be OperSymbol of S; OSALG_1:def 21 ( not o1 <= o2 or (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) )
assume A1:
o1 <= o2
; (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R)))
A2:
Args (o1,(QuotOSAlg (U1,R))) c= Args (o2,(QuotOSAlg (U1,R)))
by A1, OSALG_1:26;
Den (o2,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o2
by MSUALG_1:def 6;
then A3:
Den (o2,(QuotOSAlg (U1,R))) = OSQuotCharact (R,o2)
by Def19;
o2 in the carrier' of S
;
then A4:
o2 in dom the ResultSort of S
by FUNCT_2:def 1;
Den (o1,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o1
by MSUALG_1:def 6;
then A5:
Den (o1,(QuotOSAlg (U1,R))) = OSQuotCharact (R,o1)
by Def19;
o1 in the carrier' of S
;
then A6:
o1 in dom the ResultSort of S
by FUNCT_2:def 1;
A7:
the_arity_of o1 <= the_arity_of o2
by A1;
then
len (the_arity_of o1) = len (the_arity_of o2)
;
then A8:
dom (the_arity_of o1) = dom (the_arity_of o2)
by FINSEQ_3:29;
A9:
the_result_sort_of o1 <= the_result_sort_of o2
by A1;
then A10:
O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2)
by OSALG_1:def 17;
A11:
for x being object st x in dom (Den (o1,(QuotOSAlg (U1,R)))) holds
(Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x
proof
let x be
object ;
( x in dom (Den (o1,(QuotOSAlg (U1,R)))) implies (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x )
assume
x in dom (Den (o1,(QuotOSAlg (U1,R))))
;
(Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x
then A12:
x in Args (
o1,
(QuotOSAlg (U1,R)))
;
then A13:
x in (((OSClass R) #) * the Arity of S) . o1
by MSUALG_1:def 4;
then consider a1 being
Element of
Args (
o1,
U1)
such that A14:
x = R #_os a1
by Th14;
Result (
o1,
U1) =
( the Sorts of U1 * the ResultSort of S) . o1
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . o1)
by A6, FUNCT_1:13
.=
the
Sorts of
U1 . (the_result_sort_of o1)
by MSUALG_1:def 2
;
then reconsider da1 =
(Den (o1,U1)) . a1 as
Element of the
Sorts of
U1 . (the_result_sort_of o1) ;
reconsider da12 =
da1 as
Element of the
Sorts of
U1 . (the_result_sort_of o2) by A10;
a1 in Args (
o1,
U1)
;
then
a1 in dom (Den (o1,U1))
by FUNCT_2:def 1;
then A15:
((OSQuotRes (R,o1)) * (Den (o1,U1))) . a1 =
(OSQuotRes (R,o1)) . da1
by FUNCT_1:13
.=
OSClass (
R,
da1)
by Def14
;
A16:
(OSQuotCharact (R,o1)) . (R #_os a1) = ((OSQuotRes (R,o1)) * (Den (o1,U1))) . a1
by A13, A14, Def18;
x in Args (
o2,
(QuotOSAlg (U1,R)))
by A2, A12;
then A17:
x in (((OSClass R) #) * the Arity of S) . o2
by MSUALG_1:def 4;
then consider a2 being
Element of
Args (
o2,
U1)
such that A18:
x = R #_os a2
by Th14;
for
y being
Nat st
y in dom a1 holds
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
proof
let y be
Nat;
( y in dom a1 implies [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) )
assume A19:
y in dom a1
;
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
A20:
y in dom (the_arity_of o1)
by A19, MSUALG_6:2;
then consider z1 being
Element of the
Sorts of
U1 . ((the_arity_of o1) /. y) such that A21:
z1 = a1 . y
and A22:
(R #_os a1) . y = OSClass (
R,
z1)
by Def13;
reconsider s1 =
(the_arity_of o1) . y,
s2 =
(the_arity_of o2) . y as
SortSymbol of
S by A8, A20, PARTFUN1:4;
A23:
y in dom (the_arity_of o2)
by A8, A19, MSUALG_6:2;
then A24:
(the_arity_of o2) /. y = (the_arity_of o2) . y
by PARTFUN1:def 6;
A25:
(
(the_arity_of o1) /. y = (the_arity_of o1) . y &
s1 <= s2 )
by A7, A20, PARTFUN1:def 6;
then
the
Sorts of
U1 . ((the_arity_of o1) /. y) c= the
Sorts of
U1 . ((the_arity_of o2) /. y)
by A24, OSALG_1:def 17;
then reconsider z12 =
z1 as
Element of the
Sorts of
U1 . ((the_arity_of o2) /. y) ;
consider z2 being
Element of the
Sorts of
U1 . ((the_arity_of o2) /. y) such that A26:
z2 = a2 . y
and A27:
(R #_os a2) . y = OSClass (
R,
z2)
by A23, Def13;
OSClass (
R,
z2)
= OSClass (
R,
z12)
by A14, A18, A22, A27, A24, A25, Th4;
hence
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
by A21, A26, Th12;
verum
end;
then A28:
[((Den (o1,U1)) . a1),((Den (o2,U1)) . a2)] in R . (the_result_sort_of o2)
by A1, Def26;
Result (
o2,
U1) =
( the Sorts of U1 * the ResultSort of S) . o2
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . o2)
by A4, FUNCT_1:13
.=
the
Sorts of
U1 . (the_result_sort_of o2)
by MSUALG_1:def 2
;
then reconsider da2 =
(Den (o2,U1)) . a2 as
Element of the
Sorts of
U1 . (the_result_sort_of o2) ;
a2 in Args (
o2,
U1)
;
then
a2 in dom (Den (o2,U1))
by FUNCT_2:def 1;
then A29:
((OSQuotRes (R,o2)) * (Den (o2,U1))) . a2 =
(OSQuotRes (R,o2)) . da2
by FUNCT_1:13
.=
OSClass (
R,
da2)
by Def14
;
OSClass (
R,
da1) =
OSClass (
R,
da12)
by A9, Th4
.=
OSClass (
R,
da2)
by A28, Th12
;
hence
(Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x
by A5, A3, A17, A14, A18, A16, A15, A29, Def18;
verum
end;
( dom (Den (o2,(QuotOSAlg (U1,R)))) = Args (o2,(QuotOSAlg (U1,R))) & dom (Den (o1,(QuotOSAlg (U1,R)))) = Args (o1,(QuotOSAlg (U1,R))) )
by FUNCT_2:def 1;
then
dom (Den (o1,(QuotOSAlg (U1,R)))) = (dom (Den (o2,(QuotOSAlg (U1,R))))) /\ (Args (o1,(QuotOSAlg (U1,R))))
by A2, XBOOLE_1:28;
hence
(Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R)))
by A11, FUNCT_1:46; verum