let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
let F be ManySortedFunction of A,B; :: thesis: for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
let X be ManySortedSubset of A; :: thesis: rngs (F || X) c= rngs F
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (rngs (F || X)) . i c= (rngs F) . i )
A1: dom (F || X) = I by PARTFUN1:def 2;
assume A2: i in I ; :: thesis: (rngs (F || X)) . i c= (rngs F) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
dom F = I by PARTFUN1:def 2;
then A3: (rngs F) . i = rng f by A2, FUNCT_6:22;
(F || X) . i = f | (X . i) by A2, MSAFREE:def 1;
then (rngs (F || X)) . i = rng (f | (X . i)) by A2, A1, FUNCT_6:22;
hence (rngs (F || X)) . i c= (rngs F) . i by A3, RELAT_1:70; :: thesis: verum