let M1, M2 be compositional ManySortedFunction of ; :: thesis: M1 = M2

now

let i, j be set ; :: 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:106;
then [i,j] in dom M1 by PARTFUN1:def 4;
then consider f1, g1 being Function such that
A2: [i,j] = [g1,f1] and
A3: M1 . [i,j] = g1 * f1 by Def11;
[i,j] in dom M2 by A1, PARTFUN1:def 4;
then consider f2, g2 being Function such that
A4: [i,j] = [g2,f2] and
A5: M2 . [i,j] = g2 * f2 by Def11;
( g1 = g2 & f1 = f2 ) by A2, A4, ZFMISC_1:33;
hence M1 . i,j = M2 . i,j by A3, A5; :: thesis: verum

end;

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