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