let g be Function of [:D,C:],E; :: thesis: ( g = ~ f iff for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d) )
A1: dom g = [:D,C:] by FUNCT_2:def 1;
hence ( g = ~ f implies for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d) ) by ZFMISC_1:87, Th43; :: thesis: ( ( for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d) ) implies g = ~ f )
assume A3: for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d) ; :: thesis: g = ~ f
thus A6: dom g = dom (~ f) by A1, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom g or g . b₁ = (~ f) . b₁ )
let x be object ; :: thesis: ( not x in dom g or g . x = (~ f) . x )
assume x in dom g ; :: thesis: g . x = (~ f) . x
then consider d being Element of D, c being Element of C such that
A4: x = [d,c] by SUBSET_1:43;
thus g . x = g . (d,c) by A4
.= f . (c,d) by A3
.= (~ f) . (d,c) by A1, A6, ZFMISC_1:87, Th43
.= (~ f) . x by A4 ; :: thesis: verum