let A, B be functional set ; :: thesis: for F being compositional ManySortedSet of [:A,B:]

for g, f being Function st g in A & f in B holds

F . (g,f) = g * f

let F be compositional ManySortedSet of [:A,B:]; :: thesis: for g, f being Function st g in A & f in B holds

F . (g,f) = g * f

let g, f be Function; :: thesis: ( g in A & f in B implies F . (g,f) = g * f )

assume A1: ( g in A & f in B ) ; :: thesis: F . (g,f) = g * f

dom F = [:A,B:] by PARTFUN1:def 2;

then [g,f] in dom F by A1, ZFMISC_1:87;

then consider ff, gg being Function such that

A2: [g,f] = [gg,ff] and

A3: F . [g,f] = gg * ff by Def9;

g = gg by A2, XTUPLE_0:1;

hence F . (g,f) = g * f by A2, A3, XTUPLE_0:1; :: thesis: verum

for g, f being Function st g in A & f in B holds

F . (g,f) = g * f

let F be compositional ManySortedSet of [:A,B:]; :: thesis: for g, f being Function st g in A & f in B holds

F . (g,f) = g * f

let g, f be Function; :: thesis: ( g in A & f in B implies F . (g,f) = g * f )

assume A1: ( g in A & f in B ) ; :: thesis: F . (g,f) = g * f

dom F = [:A,B:] by PARTFUN1:def 2;

then [g,f] in dom F by A1, ZFMISC_1:87;

then consider ff, gg being Function such that

A2: [g,f] = [gg,ff] and

A3: F . [g,f] = gg * ff by Def9;

g = gg by A2, XTUPLE_0:1;

hence F . (g,f) = g * f by A2, A3, XTUPLE_0:1; :: thesis: verum