let H1, H2 be ManySortedFunction of B,A; :: thesis: ( ( for i being set st i in I holds
H1 . i = (F . i) " ) & ( for i being set st i in I holds
H2 . i = (F . i) " ) implies H1 = H2 )
assume that
A8: for i being set st i in I holds
H1 . i = (F . i) " and
A9: for i being set st i in I holds
H2 . i = (F . i) " ; :: thesis: H1 = H2

now :: thesis: for i being object st i in I holds
H1 . i = H2 . i

let i be object ; :: thesis: ( i in I implies H1 . i = H2 . i )
assume A10: i in I ; :: thesis: H1 . i = H2 . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
H1 . i = f " by A8, A10;
hence H1 . i = H2 . i by A9, A10; :: thesis: verum

end;

hence H1 = H2 by PBOOLE:3; :: thesis: verum