let I be set ; :: thesis: for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G
let A, B be ManySortedSet of I; :: thesis: for F, G being ManySortedFunction of A,{B} holds F = G
let F, G be ManySortedFunction of A,{B}; :: thesis: F = G

now

let i be set ; :: thesis: ( i in I implies F . i = G . i )
assume A1: i in I ; :: thesis: F . i = G . i
then A2: {B} . i = {(B . i)} by PZFMISC1:def 1;
( F . i is Function of (A . i),({B} . i) & G . i is Function of (A . i),({B} . i) ) by A1, PBOOLE:def 15;
hence F . i = G . i by A2, FUNCT_2:51; :: thesis: verum

end;

hence F = G by PBOOLE:3; :: thesis: verum