let I be set ; :: thesis: for A, B being V8() 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 V8() 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

let i be set ; :: 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 18;
reconsider g = G . i as Function of (A . i),(B . i) by A2, PBOOLE:def 18;

now

A3: dom G = I by PARTFUN1:def 4;
consider K being ManySortedSet of I such that
A4: K in A by PBOOLE:146;
let x be set ; :: 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 4, RELAT_1:def 18;
A6: dom (i .--> x) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A7: X . i = (i .--> x) . i by A6, FUNCT_4:14
.= x by FUNCOP_1:87 ;
X in A

proof

let s be set ; :: according to PBOOLE:def 4 :: 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 A6, TARSKI:def 1;
then X . s = K . s by FUNCT_4:12;
hence X . s in A . s by A4, A8, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

then A9: F .. X = G .. X by A1;
dom F = I by PARTFUN1:def 4;
hence f . x = (F .. X) . i by A2, A7, PRALG_1:def 17
.= g . x by A2, A7, A9, A3, PRALG_1:def 17 ;
:: thesis: verum

end;

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

end;

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