theorem :: DBLSEQ_2:7

for C, D, E being set
for f being Function of [:C,D:],E holds f = ~ (~ f) by FUNCT_4:53;