per cases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;
suppose A1: ( A = {} or B = {} ) ; :: thesis: ex b1 being ManySortedFunction of [:A,B:] st b1 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;
suppose ( A <> {} & B <> {} ) ; :: thesis: ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
then reconsider A1 = A, B1 = B as functional non empty set ;
deffunc H1( 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) = H1(i,j) from ALTCAT_1:sch 2();
 M is Function-yielding
proof
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;
then reconsider M = M 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 ) )
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;
end;