let F, G be ManySortedFunction of A,A; :: thesis: ( ( for i being set st i in I holds

F . i = id (A . i) ) & ( for i being set st i in I holds

G . i = id (A . i) ) implies F = G )

assume that

A2: for i being set st i in I holds

F . i = id (A . i) and

A3: for i being set st i in I holds

G . i = id (A . i) ; :: thesis: F = G

hence F = G by A4, FUNCT_1:2; :: thesis: verum

F . i = id (A . i) ) & ( for i being set st i in I holds

G . i = id (A . i) ) implies F = G )

assume that

A2: for i being set st i in I holds

F . i = id (A . i) and

A3: for i being set st i in I holds

G . i = id (A . i) ; :: thesis: F = G

A4: now :: thesis: for i being object st i in I holds

F . i = G . i

( dom F = I & dom G = I )
by PARTFUN1:def 2;F . i = G . i

let i be object ; :: thesis: ( i in I implies F . i = G . i )

assume A5: i in I ; :: thesis: F . i = G . i

then F . i = id (A . i) by A2;

hence F . i = G . i by A3, A5; :: thesis: verum

end;assume A5: i in I ; :: thesis: F . i = G . i

then F . i = id (A . i) by A2;

hence F . i = G . i by A3, A5; :: thesis: verum

hence F = G by A4, FUNCT_1:2; :: thesis: verum