set h = h2 ** h1;
( dom h1 = I & dom h2 = I ) by PBOOLE:def 3;
then A1: dom (h2 ** h1) = I /\ I by PBOOLE:def 24
.= I ;
then reconsider h = h2 ** h1 as ManySortedSet of I by PBOOLE:def 3;
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 Relation of A . i,A . i )
assume A2: i in I ; :: thesis: h . i is Relation of 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 Relation of A . i,A . i ; :: thesis: verum

end;

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