set pr = product B;

set ca = ComAr O;

let f, g be non empty homogeneous quasi_total PartFunc of ((product B) *),(product B); :: thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds

( ( dom p = {} implies f . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

f . p = O .. (curry w) ) ) ) & dom g = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom g holds

( ( dom p = {} implies g . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

g . p = O .. (curry w) ) ) ) implies f = g )

assume that

A33: dom f = (ComAr O) -tuples_on (product B) and

A34: for p being Element of (product B) * st p in dom f holds

( ( dom p = {} implies f . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

f . p = O .. (curry w) ) ) and

A35: dom g = (ComAr O) -tuples_on (product B) and

A36: for p being Element of (product B) * st p in dom g holds

( ( dom p = {} implies g . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

g . p = O .. (curry w) ) ) ; :: thesis: f = g

for x being object st x in (ComAr O) -tuples_on (product B) holds

f . x = g . x

set ca = ComAr O;

let f, g be non empty homogeneous quasi_total PartFunc of ((product B) *),(product B); :: thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds

( ( dom p = {} implies f . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

f . p = O .. (curry w) ) ) ) & dom g = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom g holds

( ( dom p = {} implies g . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

g . p = O .. (curry w) ) ) ) implies f = g )

assume that

A33: dom f = (ComAr O) -tuples_on (product B) and

A34: for p being Element of (product B) * st p in dom f holds

( ( dom p = {} implies f . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

f . p = O .. (curry w) ) ) and

A35: dom g = (ComAr O) -tuples_on (product B) and

A36: for p being Element of (product B) * st p in dom g holds

( ( dom p = {} implies g . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

g . p = O .. (curry w) ) ) ; :: thesis: f = g

for x being object st x in (ComAr O) -tuples_on (product B) holds

f . x = g . x

proof

hence
f = g
by A33, A35; :: thesis: verum
let x be object ; :: thesis: ( x in (ComAr O) -tuples_on (product B) implies f . x = g . x )

assume A37: x in (ComAr O) -tuples_on (product B) ; :: thesis: f . x = g . x

then consider s being Element of (product B) * such that

A38: x = s and

len s = ComAr O ;

end;assume A37: x in (ComAr O) -tuples_on (product B) ; :: thesis: f . x = g . x

then consider s being Element of (product B) * such that

A38: x = s and

len s = ComAr O ;