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: ( dom F = I & dom G = I ) by PARTFUN1:def 4;

now

let i be set ; :: thesis: ( i in I implies F . i = G . i )
assume i in I ; :: thesis: F . i = G . i
then ( F . i = id (A . i) & G . i = id (A . i) ) by A2, A3;
hence F . i = G . i ; :: thesis: verum

end;

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