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

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

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

end;

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