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

now :: thesis: for i being object st i in I holds
F . i = G . i

let i be object ; :: thesis: ( i in I implies F . i = G . i )
assume A2: i in I ; :: thesis: F . i = G . i
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: for x being object st x in A . i holds
f . x = g . x

consider K being ManySortedSet of I such that
A4: K in A by PBOOLE:134;
let x be object ; :: thesis: ( x in A . i implies f . x = g . x )
assume A5: x in A . i ; :: thesis: f . x = g . x
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: ( not s in I or X . s in A . s )
assume A8: s in I ; :: thesis: X . s in A . s

per cases ( s = i or s <> i ) ;

suppose s = i ; :: thesis: X . s in A . s

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

end;

suppose s <> i ; :: thesis: X . s in A . s

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: verum

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: verum

end;

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

end;

hence F = G ; :: thesis: verum