let f be Function; :: thesis: ~ (~ f) c= f

A1: now

let x be set ; :: thesis: ( x in dom (~ (~ f)) implies ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) )
assume x in dom (~ (~ f)) ; :: thesis: ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
then consider y2, z2 being set such that
A2: x = [z2,y2] and
A3: [y2,z2] in dom (~ f) by Def2;
take y2 = y2; :: thesis: ex z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
take z2 = z2; :: thesis: ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
thus ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A2, A3, Th43; :: thesis: verum

end;

A4: dom (~ (~ f)) c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (~ (~ f)) or x in dom f )
assume x in dom (~ (~ f)) ; :: thesis: x in dom f
then ex y2, z2 being set st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A1;
hence x in dom f ; :: thesis: verum

end;

for x being set st x in dom (~ (~ f)) holds
(~ (~ f)) . x = f . x

proof

let x be set ; :: thesis: ( x in dom (~ (~ f)) implies (~ (~ f)) . x = f . x )
assume x in dom (~ (~ f)) ; :: thesis: (~ (~ f)) . x = f . x
then consider y2, z2 being set such that
A5: x = [z2,y2] and
A6: [y2,z2] in dom (~ f) and
A7: [z2,y2] in dom f by A1;
(~ (~ f)) . z2,y2 = (~ f) . y2,z2 by A6, Def2
.= f . z2,y2 by A7, Def2 ;
hence (~ (~ f)) . x = f . x by A5; :: thesis: verum

end;

hence ~ (~ f) c= f by A4, GRFUNC_1:8; :: thesis: verum