let I be set ; :: thesis: for f being ManySortedFunction of I
for X being ManySortedSet of I holds f .:.: X c= rngs f
let f be ManySortedFunction of I; :: thesis: for X being ManySortedSet of I holds f .:.: X c= rngs f
let X be ManySortedSet of I; :: thesis: f .:.: X c= rngs f
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (f .:.: X) . i c= (rngs f) . i )
assume A1: i in I ; :: thesis: (f .:.: X) . i c= (rngs f) . i
then (f .:.: X) . i = (f . i) .: (X . i) by PBOOLE:def 20;
then (f .:.: X) . i c= rng (f . i) by RELAT_1:111;
hence (f .:.: X) . i c= (rngs f) . i by A1, MSSUBFAM:13; :: thesis: verum