let I be set ; :: thesis: for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
let f be ManySortedFunction of I; :: thesis: f .:.: (doms f) = rngs f

now :: thesis: for i being object st i in I holds
(f .:.: (doms f)) . i = (rngs f) . i

let i be object ; :: thesis: ( i in I implies (f .:.: (doms f)) . i = (rngs f) . i )
assume A1: i in I ; :: thesis: (f .:.: (doms f)) . i = (rngs f) . i
hence (f .:.: (doms f)) . i = (f . i) .: ((doms f) . i) by PBOOLE:def 20
.= (f . i) .: (dom (f . i)) by A1, MSSUBFAM:14
.= rng (f . i) by RELAT_1:113
.= (rngs f) . i by A1, MSSUBFAM:13 ;
:: thesis: verum

end;

hence f .:.: (doms f) = rngs f ; :: thesis: verum