let I be set ; :: thesis: for A, B being ManySortedSet of I
for f, g being Function st rngs (f -MSF (I,A)) c= B holds
(g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))
let A, B be ManySortedSet of I; :: thesis: for f, g being Function st rngs (f -MSF (I,A)) c= B holds
(g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))
let f, g be Function; :: thesis: ( rngs (f -MSF (I,A)) c= B implies (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) )
assume A1: rngs (f -MSF (I,A)) c= B ; :: thesis: (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))
A2: I /\ I = I ;
( dom (g -MSF (I,B)) = I & dom (f -MSF (I,A)) = I ) by PARTFUN1:def 4;
then A3: dom ((g -MSF (I,B)) ** (f -MSF (I,A))) = I by A2, PBOOLE:def 24;

A4: now

let i be set ; :: thesis: ( i in I implies ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i )
assume A5: i in I ; :: thesis: ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i
then A6: (f -MSF (I,A)) . i = f | (A . i) by Def1;
dom (f -MSF (I,A)) = I by PARTFUN1:def 4;
then (rngs (f -MSF (I,A))) . i = rng (f | (A . i)) by A5, A6, FUNCT_6:31;
then rng (f | (A . i)) c= B . i by A1, A5, PBOOLE:def 5;
then ( (g * f) | (A . i) = g * (f | (A . i)) & (B . i) | (f | (A . i)) = f | (A . i) ) by RELAT_1:112, RELAT_1:125;
then A7: (g * f) | (A . i) = (g | (B . i)) * (f | (A . i)) by MONOID_1:2;
( ((g * f) -MSF (I,A)) . i = (g * f) | (A . i) & (g -MSF (I,B)) . i = g | (B . i) ) by A5, Def1;
hence ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i by A3, A5, A6, A7, PBOOLE:def 24; :: thesis: verum

end;

dom ((g * f) -MSF (I,A)) = I by PARTFUN1:def 4;
hence (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) by A3, A4, FUNCT_1:9; :: thesis: verum