let M1, M2 be compositional ManySortedFunction of [:B,A:]; :: thesis: M1 = M2

now :: thesis: for i, j being object st i in B & j in A holds
M1 . (i,j) = M2 . (i,j)

let i, j be object ; :: thesis: ( i in B & j in A implies M1 . (i,j) = M2 . (i,j) )
assume ( i in B & j in A ) ; :: thesis: M1 . (i,j) = M2 . (i,j)
then A1: [i,j] in [:B,A:] by ZFMISC_1:87;
then [i,j] in dom M1 by PARTFUN1:def 2;
then consider f1, g1 being Function such that
A2: [i,j] = [g1,f1] and
A3: M1 . [i,j] = g1 * f1 by Def9;
[i,j] in dom M2 by A1, PARTFUN1:def 2;
then consider f2, g2 being Function such that
A4: [i,j] = [g2,f2] and
A5: M2 . [i,j] = g2 * f2 by Def9;
g1 = g2 by A2, A4, XTUPLE_0:1;
hence M1 . (i,j) = M2 . (i,j) by A2, A3, A4, A5, XTUPLE_0:1; :: thesis: verum

end;

hence M1 = M2 by Th2; :: thesis: verum