let I be set ; 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; 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; ( 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
; (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 2;
then A3:
dom ((g -MSF (I,B)) ** (f -MSF (I,A))) = I
by A2, PBOOLE:def 19;
A4:
now for i being object st i in I holds
((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . ilet i be
object ;
( i in I implies ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i )assume A5:
i in I
;
((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . ithen A6:
(f -MSF (I,A)) . i = f | (A . i)
by Def1;
dom (f -MSF (I,A)) = I
by PARTFUN1:def 2;
then
(rngs (f -MSF (I,A))) . i = rng (f | (A . i))
by A5, A6, FUNCT_6:22;
then
rng (f | (A . i)) c= B . i
by A1, A5;
then
(
(g * f) | (A . i) = g * (f | (A . i)) &
(B . i) |` (f | (A . i)) = f | (A . i) )
by RELAT_1:83, RELAT_1:94;
then A7:
(g * f) | (A . i) = (g | (B . i)) * (f | (A . i))
by MONOID_1:1;
(
((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 19;
verum end;
dom ((g * f) -MSF (I,A)) = I
by PARTFUN1:def 2;
hence
(g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))
by A3, A4, FUNCT_1:2; verum