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