let O1, O2 be equal-arity ManySortedOperation of Carrier A; :: thesis: ( ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O1 . j = o ) & ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O2 . j = o ) implies O1 = O2 )
assume that
A9: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O1 . j = o and
A10: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
O2 . j = o ; :: thesis: O1 = O2
for x being object st x in J holds
O1 . x = O2 . x

proof

let x be object ; :: thesis: ( x in J implies O1 . x = O2 . x )
assume x in J ; :: thesis: O1 . x = O2 . x
then reconsider x1 = x as Element of J ;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def 3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def 4;
then n in dom the charact of (A . x1) by FINSEQ_1:def 3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def 3;
O1 . x1 = o by A9;
hence O1 . x = O2 . x by A10; :: thesis: verum

end;

hence O1 = O2 ; :: thesis: verum