set h = h2 ** h1;
A1: dom h2 = I by PARTFUN1:def 2;
dom h1 = I by PARTFUN1:def 2;
then A2: dom (h2 ** h1) = I /\ I by A1, PBOOLE:def 19
.= I ;
then reconsider h = h2 ** h1 as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
h is ManySortedFunction of A,A
proof
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or h . i is Element of bool [:(A . i),(A . i):] )
assume A3: 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 15;
h . i = g * f by A2, A3, PBOOLE:def 19;
hence h . i is Element of bool [:(A . i),(A . i):] ; :: thesis: verum
end;
hence h2 ** h1 is ManySortedFunction of A,A ; :: thesis: verum