let q1, q2 be Element of Args (o,Q); :: thesis: ( ( for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q1 . i = A / (x,y) ) ) ) & ( for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q2 . i = A / (x,y) ) ) ) implies q1 = q2 )

assume that

A5: for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q1 . i = A / (x,y) ) ) and

A6: for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q2 . i = A / (x,y) ) ) ; :: thesis: q1 = q2

A7: ( dom q1 = dom (the_arity_of o) & dom q2 = dom (the_arity_of o) ) by MSUALG_6:2;

hence dom q1 = dom q2 ; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom q1 or q1 . b_{1} = q2 . b_{1} )

let z be object ; :: thesis: ( not z in dom q1 or q1 . z = q2 . z )

assume A8: z in dom q1 ; :: thesis: q1 . z = q2 . z

then reconsider i = z as Nat ;

consider j1 being SortSymbol of J such that

A9: ( j1 = (the_arity_of o) . i & ex A being Element of Q,j1 st

( A = p . i & q1 . i = A / (x,y) ) ) by A5, A7, A8;

consider j2 being SortSymbol of J such that

A10: ( j2 = (the_arity_of o) . i & ex A being Element of Q,j2 st

( A = p . i & q2 . i = A / (x,y) ) ) by A6, A7, A8;

thus q1 . z = q2 . z by A9, A10; :: thesis: verum

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q1 . i = A / (x,y) ) ) ) & ( for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q2 . i = A / (x,y) ) ) ) implies q1 = q2 )

assume that

A5: for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q1 . i = A / (x,y) ) ) and

A6: for i being Nat st i in dom (the_arity_of o) holds

ex j being SortSymbol of J st

( j = (the_arity_of o) . i & ex A being Element of Q,j st

( A = p . i & q2 . i = A / (x,y) ) ) ; :: thesis: q1 = q2

A7: ( dom q1 = dom (the_arity_of o) & dom q2 = dom (the_arity_of o) ) by MSUALG_6:2;

hence dom q1 = dom q2 ; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let z be object ; :: thesis: ( not z in dom q1 or q1 . z = q2 . z )

assume A8: z in dom q1 ; :: thesis: q1 . z = q2 . z

then reconsider i = z as Nat ;

consider j1 being SortSymbol of J such that

A9: ( j1 = (the_arity_of o) . i & ex A being Element of Q,j1 st

( A = p . i & q1 . i = A / (x,y) ) ) by A5, A7, A8;

consider j2 being SortSymbol of J such that

A10: ( j2 = (the_arity_of o) . i & ex A being Element of Q,j2 st

( A = p . i & q2 . i = A / (x,y) ) ) by A6, A7, A8;

thus q1 . z = q2 . z by A9, A10; :: thesis: verum