let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
~ (~ f) = f
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies ~ (~ f) = f )
assume A1: dom f c= [:X,Y:] ; :: thesis: ~ (~ f) = f
A2: ~ (~ f) c= f by Th51;
dom (~ (~ f)) = dom f

proof

thus dom (~ (~ f)) c= dom f by A2, RELAT_1:11; :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom (~ (~ f))
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom f or z in dom (~ (~ f)) )
assume A3: z in dom f ; :: thesis: z in dom (~ (~ f))
then consider x, y being object such that
x in X and
y in Y and
A4: z = [x,y] by A1, ZFMISC_1:84;
[y,x] in dom (~ f) by A3, A4, Th42;
hence z in dom (~ (~ f)) by A4, Th42; :: thesis: verum

end;

hence ~ (~ f) = f by Th51, GRFUNC_1:3; :: thesis: verum