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₁ being object holds
( not b₁ in dom q1 or q1 . b₁ = q2 . 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