theorem :: EXTENS_1:11

for I being set
for A being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being non-empty ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F