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