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

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

( dom F = I & dom G = I ) by PARTFUN1:def 2;
hence F = G by A4, FUNCT_1:2; :: thesis: verum