let i, I be set ; :: thesis: for F being ManySortedFunction of
for f being Function st i in I & f = F . i holds
(rngs F) . i = rng f
let F be ManySortedFunction of ; :: thesis: for f being Function st i in I & f = F . i holds
(rngs F) . i = rng f
let f be Function; :: thesis: ( i in I & f = F . i implies (rngs F) . i = rng f )
assume A1: ( i in I & f = F . i ) ; :: thesis: (rngs F) . i = rng f
dom F = I by PARTFUN1:def 4;
hence (rngs F) . i = rng f by A1, FUNCT_6:31; :: thesis: verum