let f be Function; ~ (~ f) c= f
A1:
now 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 ;
( 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))
;
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;
ex z2 being object st
( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f )take z2 =
z2;
( 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;
verum end;
A3:
for x being object st x in dom (~ (~ f)) holds
(~ (~ f)) . x = f . x
dom (~ (~ f)) c= dom f
hence
~ (~ f) c= f
by A3, GRFUNC_1:2; verum