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

proof

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 ;

per cases ( dom s = {} or dom s <> {} ) ;

suppose A39: dom s = {} ; :: thesis: f . x = g . x

then f . s = O .. (EmptyMS J) by A33, A34, A37, A38;
hence f . x = g . x by A35, A36, A37, A38, A39; :: thesis: verum

end;

suppose dom s <> {} ; :: thesis: f . x = g . x

then reconsider Z = dom s as non empty set ;
reconsider w = ~ (uncurry s) as ManySortedSet of [:J,Z:] ;
f . s = O .. (curry w) by A33, A34, A37, A38;
hence f . x = g . x by A35, A36, A37, A38; :: thesis: verum

end;

end;

end;

hence f = g by A33, A35; :: thesis: verum