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