let I be set ; :: thesis: for A, B, C being ManySortedSet of
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of
let A, B, C be ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of
let G be ManySortedFunction of B,C; :: thesis: G ** F is ManySortedSet 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 ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum