set pr = product B;
set ca = ComAr O;
let f, g be non empty homogeneous quasi_total PartFunc of (() *),(); :: thesis: ( dom f = () -tuples_on () & ( for p being Element of () * st p in dom f holds
( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) ) ) & dom g = () -tuples_on () & ( for p being Element of () * st p in dom g holds
( ( dom p = {} implies g . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
g . p = O .. () ) ) ) implies f = g )

assume that
A33: dom f = () -tuples_on () and
A34: for p being Element of () * st p in dom f holds
( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) ) and
A35: dom g = () -tuples_on () and
A36: for p being Element of () * st p in dom g holds
( ( dom p = {} implies g . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
g . p = O .. () ) ) ; :: thesis: f = g
for x being object st x in () -tuples_on () holds
f . x = g . x
proof
let x be object ; :: thesis: ( x in () -tuples_on () implies f . x = g . x )
assume A37: x in () -tuples_on () ; :: thesis: f . x = g . x
then consider s being Element of () * 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 .. () 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 = ~ () as ManySortedSet of [:J,Z:] ;
f . s = O .. () by A33, A34, A37, A38;
hence f . x = g . x by A35, A36, A37, A38; :: thesis: verum
end;
end;
end;
hence f = g by ; :: thesis: verum