let I be set ; :: thesis: for F, G being ManySortedFunction of holds G ** F is ManySortedFunction of
let F, G be ManySortedFunction of ; :: thesis: G ** F is ManySortedFunction of
dom (G ** F) = (dom F) /\ (dom G) by PBOOLE:def 24
.= I /\ (dom G) by PARTFUN1:def 4
.= I /\ I by PARTFUN1:def 4
.= I ;
hence G ** F is ManySortedFunction of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum