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 23 ( 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 11;
then A3:
Den o2,(QuotOSAlg U1,R) = OSQuotCharact R,o2
by Def21;
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 11;
then A5:
Den o1,(QuotOSAlg U1,R) = OSQuotCharact R,o1
by Def21;
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, OSALG_1:def 22;
then
len (the_arity_of o1) = len (the_arity_of o2)
by OSALG_1:def 7;
then A8:
dom (the_arity_of o1) = dom (the_arity_of o2)
by FINSEQ_3:31;
A9:
the_result_sort_of o1 <= the_result_sort_of o2
by A1, OSALG_1:def 22;
then A10:
O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2)
by OSALG_1:def 19;
A11:
for x being set 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
set ;
( 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 9;
then consider a1 being
Element of
Args o1,
U1 such that A14:
x = R #_os a1
by Th15;
Result o1,
U1 =
(the Sorts of U1 * the ResultSort of S) . o1
by MSUALG_1:def 10
.=
the
Sorts of
U1 . (the ResultSort of S . o1)
by A6, FUNCT_1:23
.=
the
Sorts of
U1 . (the_result_sort_of o1)
by MSUALG_1:def 7
;
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, TARSKI:def 3;
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:23
.=
OSClass R,
da1
by Def16
;
A16:
(OSQuotCharact R,o1) . (R #_os a1) = ((OSQuotRes R,o1) * (Den o1,U1)) . a1
by A13, A14, Def20;
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 9;
then consider a2 being
Element of
Args o2,
U1 such that A18:
x = R #_os a2
by Th15;
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 Def15;
reconsider s1 =
(the_arity_of o1) . y,
s2 =
(the_arity_of o2) . y as
SortSymbol of
S by A8, A20, PARTFUN1:27;
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 8;
A25:
(
(the_arity_of o1) /. y = (the_arity_of o1) . y &
s1 <= s2 )
by A7, A20, OSALG_1:def 7, PARTFUN1:def 8;
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 19;
then reconsider z12 =
z1 as
Element of the
Sorts of
U1 . ((the_arity_of o2) /. y) by TARSKI:def 3;
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, Def15;
OSClass R,
z2 = OSClass R,
z12
by A14, A18, A22, A27, A24, A25, Th5;
hence
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
by A21, A26, Th13;
verum
end;
then A28:
[((Den o1,U1) . a1),((Den o2,U1) . a2)] in R . (the_result_sort_of o2)
by A1, Def28;
Result o2,
U1 =
(the Sorts of U1 * the ResultSort of S) . o2
by MSUALG_1:def 10
.=
the
Sorts of
U1 . (the ResultSort of S . o2)
by A4, FUNCT_1:23
.=
the
Sorts of
U1 . (the_result_sort_of o2)
by MSUALG_1:def 7
;
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:23
.=
OSClass R,
da2
by Def16
;
OSClass R,
da1 =
OSClass R,
da12
by A9, Th5
.=
OSClass R,
da2
by A28, Th13
;
hence
(Den o1,(QuotOSAlg U1,R)) . x = (Den o2,(QuotOSAlg U1,R)) . x
by A5, A3, A17, A14, A18, A16, A15, A29, Def20;
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:68; verum