let q1, q2 be Element of Args (o,Q); :: thesis: ( ( for i being Nat st i in dom () holds
ex j being SortSymbol of J st
( j = () . 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 () holds
ex j being SortSymbol of J st
( j = () . 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 () holds
ex j being SortSymbol of J st
( j = () . 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 () holds
ex j being SortSymbol of J st
( j = () . i & ex A being Element of Q,j st
( A = p . i & q2 . i = A / (x,y) ) ) ; :: thesis: q1 = q2
A7: ( dom q1 = dom () & dom q2 = dom () ) by MSUALG_6:2;
hence dom q1 = dom q2 ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom q1 or q1 . b1 = q2 . b1 )

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 = () . 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 = () . 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 ; :: thesis: verum