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 .. (EmptySeq B) ) & ( 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 .. (EmptySeq B) ) & ( 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
A27: ( 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 .. (EmptySeq B) ) & ( 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
A28: ( 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 .. (EmptySeq B) ) & ( 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 set st x in (ComAr O) -tuples_on (product B) holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in (ComAr O) -tuples_on (product B) implies f . x = g . x )
assume A29: x in (ComAr O) -tuples_on (product B) ; :: thesis: f . x = g . x
then consider s being Element of (product B) * such that
A30: ( x = s & len s = ComAr O ) ;

now

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

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

then ( f . s = O .. (EmptySeq B) & g . s = O .. (EmptySeq B) ) by A27, A28, A29, A30;
hence f . x = g . x by A30; :: thesis: verum

end;

case 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) & g . s = O .. (curry w) ) by A27, A28, A29, A30;
hence f . x = g . x by A30; :: thesis: verum

end;

end;

end;

hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A27, A28, FUNCT_1:9; :: thesis: verum