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 :: 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 ;
now :: thesis: for x being object st x in A . i holds
f . x = g . x
A3: dom G = I by PARTFUN1:def 2;
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 ;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by ;
A6: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A7: X . i = (i .--> x) . i by
.= 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;
dom F = I by PARTFUN1:def 2;
hence f . x = (F .. X) . i by
.= g . x by ;
:: thesis: verum
end;
hence F . i = G . i by FUNCT_2:12; :: thesis: verum
end;
hence F = G ; :: thesis: verum