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

let i be set ; :: 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 18;
( H1 . i = f " & H2 . i = f " ) by A8, A9, A10;
hence H1 . i = H2 . i ; :: thesis: verum

end;

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