let g be Function of [:D,C:],E; ( 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; ( ( 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)
; g = ~ f
thus A6:
dom g = dom (~ f)
by A1, FUNCT_2:def 1; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom g or g . b1 = (~ f) . b1 )
let x be object ; ( not x in dom g or g . x = (~ f) . x )
assume
x in dom g
; 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
; verum