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)

hence
M1 = M2
by Th2; :: thesis: verumM1 . (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;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