let I be set ; :: thesis: for F, G being ManySortedFunction of I
for A being ManySortedSet of I st A in doms G holds
F .. (G .. A) = (F ** G) .. A
let F, G be ManySortedFunction of I; :: thesis: for A being ManySortedSet of I st A in doms G holds
F .. (G .. A) = (F ** G) .. A
A1: dom F = I by PARTFUN1:def 2;
reconsider FG = F ** G as ManySortedFunction of I by MSSUBFAM:15;
A2: dom G = I by PARTFUN1:def 2;
A3: dom FG = I by PARTFUN1:def 2;
let A be ManySortedSet of I; :: thesis: ( A in doms G implies F .. (G .. A) = (F ** G) .. A )
assume A4: A in doms G ; :: thesis: F .. (G .. A) = (F ** G) .. A

A5: now

let i be set ; :: thesis: ( i in I implies (F .. (G .. A)) . i = ((F ** G) .. A) . i )
reconsider f = F . i as Function ;
reconsider g = G . i as Function ;
reconsider fg = (F ** G) . i as Function ;
assume A6: i in I ; :: thesis: (F .. (G .. A)) . i = ((F ** G) .. A) . i
then dom g = (doms G) . i by MSSUBFAM:14;
then A7: A . i in dom g by A4, A6, PBOOLE:def 1;
(G .. A) . i = g . (A . i) by A2, A6, PRALG_1:def 17;
hence (F .. (G .. A)) . i = f . (g . (A . i)) by A1, A6, PRALG_1:def 17
.= (f * g) . (A . i) by A7, FUNCT_1:13
.= fg . (A . i) by A3, A6, PBOOLE:def 19
.= ((F ** G) .. A) . i by A3, A6, PRALG_1:def 17 ;
:: thesis: verum

end;

FG .. A is ManySortedSet of I ;
hence F .. (G .. A) = (F ** G) .. A by A5, PBOOLE:3; :: thesis: verum