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

A1: now :: thesis: for x being object st x in dom (~ (~ f)) holds
ex y2, z2 being object st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )

let x be object ; :: thesis: ( x in dom (~ (~ f)) implies ex y2, z2 being object st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) )
assume x in dom (~ (~ f)) ; :: thesis: ex y2, z2 being object st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )
then consider y2, z2 being object such that
A2: ( x = [z2,y2] & [y2,z2] in dom (~ f) ) by Def2;
take y2 = y2; :: thesis: ex z2 being object 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, Th42; :: thesis: verum

end;

A3: for x being object st x in dom (~ (~ f)) holds
(~ (~ f)) . x = f . x

proof

let x be object ; :: 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 object such that
A4: x = [z2,y2] and
A5: [y2,z2] in dom (~ f) and
A6: [z2,y2] in dom f by A1;
(~ (~ f)) . (z2,y2) = (~ f) . (y2,z2) by A5, Def2
.= f . (z2,y2) by A6, Def2 ;
hence (~ (~ f)) . x = f . x by A4; :: thesis: verum

end;

dom (~ (~ f)) c= dom f

proof

let x be object ; :: 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 object st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A1;
hence x in dom f ; :: thesis: verum

end;

hence ~ (~ f) c= f by A3, GRFUNC_1:2; :: thesis: verum