set A = QuotOSAlg U1,R;
reconsider O1 = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
let o1, o2 be OperSymbol of S; :: according to OSALG_1:def 23 :: thesis: ( not o1 <= o2 or (Den o2,(QuotOSAlg U1,R)) | (Args o1,(QuotOSAlg U1,R)) = Den o1,(QuotOSAlg U1,R) )
assume A1:
o1 <= o2
; :: thesis: (Den o2,(QuotOSAlg U1,R)) | (Args o1,(QuotOSAlg U1,R)) = Den o1,(QuotOSAlg U1,R)
A2:
( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 )
by A1, OSALG_1:def 22;
A3:
( 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;
A4:
( Args o1,(QuotOSAlg U1,R) c= Args o2,(QuotOSAlg U1,R) & Result o1,(QuotOSAlg U1,R) c= Result o2,(QuotOSAlg U1,R) )
by A1, OSALG_1:26;
then A5:
dom (Den o1,(QuotOSAlg U1,R)) = (dom (Den o2,(QuotOSAlg U1,R))) /\ (Args o1,(QuotOSAlg U1,R))
by A3, XBOOLE_1:28;
( Den o1,(QuotOSAlg U1,R) = (OSQuotCharact R) . o1 & Den o2,(QuotOSAlg U1,R) = (OSQuotCharact R) . o2 )
by MSUALG_1:def 11;
then A6:
( Den o1,(QuotOSAlg U1,R) = OSQuotCharact R,o1 & Den o2,(QuotOSAlg U1,R) = OSQuotCharact R,o2 )
by Def21;
A7:
O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2)
by A2, OSALG_1:def 19;
( o1 in the carrier' of S & o2 in the carrier' of S )
;
then A8:
( o1 in dom the ResultSort of S & o2 in dom the ResultSort of S )
by FUNCT_2:def 1;
len (the_arity_of o1) = len (the_arity_of o2)
by A2, OSALG_1:def 7;
then A9:
dom (the_arity_of o1) = dom (the_arity_of o2)
by FINSEQ_3:31;
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 ;
:: thesis: ( x in dom (Den o1,(QuotOSAlg U1,R)) implies (Den o1,(QuotOSAlg U1,R)) . x = (Den o2,(QuotOSAlg U1,R)) . x )
assume A10:
x in dom (Den o1,(QuotOSAlg U1,R))
;
:: thesis: (Den o1,(QuotOSAlg U1,R)) . x = (Den o2,(QuotOSAlg U1,R)) . x
A11:
x in Args o1,
(QuotOSAlg U1,R)
by A10;
then
x in Args o2,
(QuotOSAlg U1,R)
by A4;
then A12:
(
x in (((OSClass R) # ) * the Arity of S) . o1 &
x in (((OSClass R) # ) * the Arity of S) . o2 )
by A11, MSUALG_1:def 9;
then consider a1 being
Element of
Args o1,
U1 such that A13:
x = R #_os a1
by Th15;
consider a2 being
Element of
Args o2,
U1 such that A14:
x = R #_os a2
by A12, 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;
:: thesis: ( y in dom a1 implies [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) )
assume A15:
y in dom a1
;
:: thesis: [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
A16:
(
y in dom (the_arity_of o1) &
y in dom (the_arity_of o2) )
by A9, A15, MSUALG_6:2;
then consider z1 being
Element of the
Sorts of
U1 . ((the_arity_of o1) /. y) such that A17:
(
z1 = a1 . y &
(R #_os a1) . y = OSClass R,
z1 )
by Def15;
consider z2 being
Element of the
Sorts of
U1 . ((the_arity_of o2) /. y) such that A18:
(
z2 = a2 . y &
(R #_os a2) . y = OSClass R,
z2 )
by A16, Def15;
A19:
(
(the_arity_of o1) /. y = (the_arity_of o1) . y &
(the_arity_of o2) /. y = (the_arity_of o2) . y )
by A16, PARTFUN1:def 8;
reconsider s1 =
(the_arity_of o1) . y,
s2 =
(the_arity_of o2) . y as
SortSymbol of
S by A16, PARTFUN1:27;
A20:
s1 <= s2
by A2, A16, OSALG_1:def 7;
then
the
Sorts of
U1 . ((the_arity_of o1) /. y) c= the
Sorts of
U1 . ((the_arity_of o2) /. y)
by A19, OSALG_1:def 19;
then reconsider z12 =
z1 as
Element of the
Sorts of
U1 . ((the_arity_of o2) /. y) by TARSKI:def 3;
OSClass R,
z2 = OSClass R,
z12
by A13, A14, A17, A18, A19, A20, Th5;
hence
[(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y)
by A17, A18, Th13;
:: thesis: verum
end;
then A21:
[((Den o1,U1) . a1),((Den o2,U1) . a2)] in R . (the_result_sort_of o2)
by A1, Def28;
A22:
(
(OSQuotCharact R,o1) . (R #_os a1) = ((OSQuotRes R,o1) * (Den o1,U1)) . a1 &
(OSQuotCharact R,o2) . (R #_os a2) = ((OSQuotRes R,o2) * (Den o2,U1)) . a2 )
by A12, A13, A14, Def20;
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 A8, 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) ;
a1 in Args o1,
U1
;
then
a1 in dom (Den o1,U1)
by FUNCT_2:def 1;
then A23:
((OSQuotRes R,o1) * (Den o1,U1)) . a1 =
(OSQuotRes R,o1) . da1
by FUNCT_1:23
.=
OSClass R,
da1
by Def16
;
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 A8, 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 A24:
((OSQuotRes R,o2) * (Den o2,U1)) . a2 =
(OSQuotRes R,o2) . da2
by FUNCT_1:23
.=
OSClass R,
da2
by Def16
;
reconsider da12 =
da1 as
Element of the
Sorts of
U1 . (the_result_sort_of o2) by A7, TARSKI:def 3;
OSClass R,
da1 =
OSClass R,
da12
by A2, Th5
.=
OSClass R,
da2
by A21, Th13
;
hence
(Den o1,(QuotOSAlg U1,R)) . x = (Den o2,(QuotOSAlg U1,R)) . x
by A6, A13, A14, A22, A23, A24;
:: thesis: verum
end;
hence
(Den o2,(QuotOSAlg U1,R)) | (Args o1,(QuotOSAlg U1,R)) = Den o1,(QuotOSAlg U1,R)
by A5, FUNCT_1:68; :: thesis: verum