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 4;
then [g,f] in dom F by A1, ZFMISC_1:106;
then consider ff, gg being Function such that
A2: [g,f] = [gg,ff] and
A3: F . [g,f] = gg * ff by Def11;
g = gg by A2, ZFMISC_1:33;
hence F . g,f = g * f by A2, A3, ZFMISC_1:33; :: thesis: verum