set h = h2 ** h1;
( dom h1 = I & dom h2 = I ) by PARTFUN1:def 4;
then A1: dom (h2 ** h1) = I /\ I by PBOOLE:def 24
.= I ;
then reconsider h = h2 ** h1 as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
h is ManySortedFunction of A,A

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I or h . i is Element of bool [:(A . i),(A . i):] )
assume A2: i in I ; :: thesis: h . i is Element of bool [:(A . i),(A . i):]
then reconsider f = h1 . i, g = h2 . i as Function of (A . i),(A . i) by PBOOLE:def 18;
h . i = g * f by A1, A2, PBOOLE:def 24;
hence h . i is Element of bool [:(A . i),(A . i):] ; :: thesis: verum

end;

hence h2 ** h1 is ManySortedFunction of A,A ; :: thesis: verum