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

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . 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

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C holds

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

let G be ManySortedFunction of B,C; :: thesis: ( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

( dom F = I & dom G = I ) by PARTFUN1:def 2;

then (dom F) /\ (dom G) = I ;

hence A1: dom (G ** F) = I by PBOOLE:def 19; :: thesis: for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i)

let i be set ; :: thesis: ( i in I implies (G ** F) . i = (G . i) * (F . i) )

thus ( i in I implies (G ** F) . i = (G . i) * (F . i) ) by A1, PBOOLE:def 19; :: thesis: verum

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C holds

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . 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

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C holds

( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

let G be ManySortedFunction of B,C; :: thesis: ( dom (G ** F) = I & ( for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i) ) )

( dom F = I & dom G = I ) by PARTFUN1:def 2;

then (dom F) /\ (dom G) = I ;

hence A1: dom (G ** F) = I by PBOOLE:def 19; :: thesis: for i being set st i in I holds

(G ** F) . i = (G . i) * (F . i)

let i be set ; :: thesis: ( i in I implies (G ** F) . i = (G . i) * (F . i) )

thus ( i in I implies (G ** F) . i = (G . i) * (F . i) ) by A1, PBOOLE:def 19; :: thesis: verum