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

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

hence
H1 = H2
by PBOOLE:3; :: thesis: verumH1 . 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;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