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