let M1, M2 be compositional ManySortedFunction of [:B,A:]; M1 = M2
now for i, j being object st i in B & j in A holds
M1 . (i,j) = M2 . (i,j)let i,
j be
object ;
( i in B & j in A implies M1 . (i,j) = M2 . (i,j) )assume
(
i in B &
j in A )
;
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;
verum end;
hence
M1 = M2
by Th2; verum