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

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

hence
O1 = O2
; :: thesis: verum
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;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