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