per cases
( A = {} or B = {} or ( A <> {} & B <> {} ) )
;

end;

suppose A1:
( A = {} or B = {} )
; :: thesis: ex b_{1} being ManySortedFunction of [:A,B:] st b_{1} is compositional

set M = EmptyMS [:A,B:];

EmptyMS [:A,B:] is Function-yielding by A1;

then reconsider M = EmptyMS [:A,B:] as ManySortedFunction of [:A,B:] ;

take M ; :: thesis: M is compositional

let x be object ; :: according to ALTCAT_1:def 9 :: thesis: ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) )

thus ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) ) by A1; :: thesis: verum

end;EmptyMS [:A,B:] is Function-yielding by A1;

then reconsider M = EmptyMS [:A,B:] as ManySortedFunction of [:A,B:] ;

take M ; :: thesis: M is compositional

let x be object ; :: according to ALTCAT_1:def 9 :: thesis: ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) )

thus ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) ) by A1; :: thesis: verum

suppose
( A <> {} & B <> {} )
; :: thesis: ex b_{1} being ManySortedFunction of [:A,B:] st b_{1} is compositional

then reconsider A1 = A, B1 = B as functional non empty set ;

deffunc H_{1}( Element of A1, Element of B1) -> set = A * B;

consider M being ManySortedSet of [:A1,B1:] such that

A2: for i being Element of A1

for j being Element of B1 holds M . (i,j) = H_{1}(i,j)
from ALTCAT_1:sch 2();

M is Function-yielding

take M ; :: thesis: M is compositional

let x be object ; :: according to ALTCAT_1:def 9 :: thesis: ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) )

assume x in dom M ; :: thesis: ex f, g being Function st

( x = [g,f] & M . x = g * f )

then A5: x in [:A1,B1:] ;

then A6: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;

then reconsider f = x `1 , g = x `2 as Function ;

take g ; :: thesis: ex g being Function st

( x = [g,g] & M . x = g * g )

take f ; :: thesis: ( x = [f,g] & M . x = f * g )

thus x = [f,g] by A5, MCART_1:22; :: thesis: M . x = f * g

thus M . x = M . (f,g) by A5, MCART_1:22

.= f * g by A2, A6 ; :: thesis: verum

end;deffunc H

consider M being ManySortedSet of [:A1,B1:] such that

A2: for i being Element of A1

for j being Element of B1 holds M . (i,j) = H

M is Function-yielding

proof

then reconsider M = M as ManySortedFunction of [:A,B:] ;
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 M or M . x is set )

assume x in dom M ; :: thesis: M . x is set

then A3: x in [:A1,B1:] ;

then A4: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;

then reconsider f = x `1 , g = x `2 as Function ;

M . x = M . (f,g) by A3, MCART_1:22

.= f * g by A2, A4 ;

hence M . x is set ; :: thesis: verum

end;assume x in dom M ; :: thesis: M . x is set

then A3: x in [:A1,B1:] ;

then A4: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;

then reconsider f = x `1 , g = x `2 as Function ;

M . x = M . (f,g) by A3, MCART_1:22

.= f * g by A2, A4 ;

hence M . x is set ; :: thesis: verum

take M ; :: thesis: M is compositional

let x be object ; :: according to ALTCAT_1:def 9 :: thesis: ( x in dom M implies ex f, g being Function st

( x = [g,f] & M . x = g * f ) )

assume x in dom M ; :: thesis: ex f, g being Function st

( x = [g,f] & M . x = g * f )

then A5: x in [:A1,B1:] ;

then A6: ( x `1 in A1 & x `2 in B1 ) by MCART_1:10;

then reconsider f = x `1 , g = x `2 as Function ;

take g ; :: thesis: ex g being Function st

( x = [g,g] & M . x = g * g )

take f ; :: thesis: ( x = [f,g] & M . x = f * g )

thus x = [f,g] by A5, MCART_1:22; :: thesis: M . x = f * g

thus M . x = M . (f,g) by A5, MCART_1:22

.= f * g by A2, A6 ; :: thesis: verum