let I be set ; :: thesis: for A, B being ManySortedSet of
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 ; :: 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: ( dom ((g * f) -MSF I,A) = I & dom (g -MSF I,B) = I & dom (f -MSF I,A) = I & I /\ I = I ) by PARTFUN1:def 4;
then A3: dom ((g -MSF I,B) ** (f -MSF I,A)) = I by PBOOLE:def 24;

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 A4: i in I ; :: thesis: ((g * f) -MSF I,A) . i = ((g -MSF I,B) ** (f -MSF I,A)) . i
then A5: ( ((g * f) -MSF I,A) . i = (g * f) | (A . i) & (f -MSF I,A) . i = f | (A . i) & (g -MSF I,B) . i = g | (B . 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 A4, A5, FUNCT_6:31;
then rng (f | (A . i)) c= B . i by A1, A4, 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 (g * f) | (A . i) = (g | (B . i)) * (f | (A . i)) by MONOID_1:2;
hence ((g * f) -MSF I,A) . i = ((g -MSF I,B) ** (f -MSF I,A)) . i by A3, A4, A5, PBOOLE:def 24; :: thesis: verum

end;

hence (g * f) -MSF I,A = (g -MSF I,B) ** (f -MSF I,A) by A2, A3, FUNCT_1:9; :: thesis: verum