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

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

hence
F = G
; :: thesis: verumF . 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;

end;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

hence
F . i = G . i
by FUNCT_2:12; :: thesis: verumf . 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 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

dom F = I by PARTFUN1:def 2;

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;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

then A9:
F .. X = G .. X
by A1;
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

end;assume A8: s in I ; :: thesis: X . s in A . s

dom F = I by PARTFUN1:def 2;

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