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 24
.= I /\ (dom G) by PBOOLE:def 3
.= I /\ I by PBOOLE:def 3
.= I ;
hence G ** F is ManySortedSet of I by PBOOLE:def 3; :: thesis: verum