let I be set ; :: thesis:
let A, B be V8() ManySortedSet of I; :: thesis:
let F, G be ManySortedFunction of A,B; :: thesis:
assume A1: for M being ManySortedSet of I st M in A holds
F .. M = G .. M ; :: thesis:

now :: thesis:

let i be object ; :: thesis:
assume A2: i in I ; :: thesis:
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider g = G . i as Function of (A . i),(B . i) by A2, PBOOLE:def 15;

now :: thesis:

consider K being ManySortedSet of I such that
A4: K in A by PBOOLE:134;
let x be object ; :: thesis:
assume A5: x in A . i ; :: thesis:
dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A6: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A7: X . i = (i .--> x) . i by A6, FUNCT_4:13
.= x by FUNCOP_1:72 ;
X in A

proof

let s be object ; :: according to PBOOLE:def 1 :: thesis:
assume A8: s in I ; :: thesis:

per cases ;

suppose s = i ; :: thesis:

hence X . s in A . s by A5, A7; :: thesis:

end;

suppose s <> i ; :: thesis:

then not s in dom (i .--> x) by TARSKI:def 1;
then X . s = K . s by FUNCT_4:11;
hence X . s in A . s by A4, A8; :: thesis:

end;

end;

end;

then A9: F .. X = G .. X by A1;
thus f . x = (F .. X) . i by A2, A7, PRALG_1:def 20
.= g . x by A2, A7, A9, PRALG_1:def 20 ; :: thesis:

end;

hence F . i = G . i by FUNCT_2:12; :: thesis:

end;

hence F = G ; :: thesis: