let I be set ; :: thesis: for A, B being V8() ManySortedSet of
for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of st M in A holds
F .. M = G .. M ) holds
F = G
let A, B be V8() ManySortedSet of ; :: thesis: for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of 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 st M in A holds
F .. M = G .. M ) implies F = G )
assume A1: for M being ManySortedSet of 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
let x be set ; :: thesis: ( x in A . i implies f . x = g . x )
assume A3: x in A . i ; :: thesis: f . x = g . x
consider K being ManySortedSet of such that
A4: K in A by PBOOLE:146;
dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A5: dom (i .--> x) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> x) . i by A5, 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 A7: 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 A3, A6; :: thesis: verum
end;
end;
end;
then A8: F .. X = G .. X by A1;
A9: dom F = I by PARTFUN1:def 4;
A10: dom G = I by PARTFUN1:def 4;
thus f . x = (F .. X) . i by A2, A6, A9, PRALG_1:def 17
.= g . x by A2, A6, A8, A10, 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