let f be Function; :: thesis: ( f is involutive & rng f c= dom f implies ( f .: (OtherPoints f) = SomePoints f & f .: (SomePoints f) = OtherPoints f ) )
assume f is involutive ; :: thesis: ( not rng f c= dom f or ( f .: (OtherPoints f) = SomePoints f & f .: (SomePoints f) = OtherPoints f ) )
then reconsider ff = f as involutive Function ;
set D = dom ff;
set C = rng ff;
set S = SomePoints ff;
set O = OtherPoints ff;
set F = fixpoints ff;
set I = id (dom ff);
reconsider g = ff * ff as Relation-like Function-like Subset of (id (dom ff)) by FOMODEL0:72;
assume rng f c= dom f ; :: thesis: ( f .: (OtherPoints f) = SomePoints f & f .: (SomePoints f) = OtherPoints f )
then reconsider C = rng ff as Subset of (dom ff) ;
( C c= dom ff & (dom ff) null C c= field f ) ;
then reconsider CC = C as Subset of (field f) ;
set D2 = dom g;
field ff = (dom ff) null C ;
then reconsider SS = SomePoints ff, OO = OtherPoints ff as Subset of (dom ff) ;
C c= dom ff ;
then reconsider SSS = SS, OOO = OO as Subset of (dom g) by RELAT_1:27;
g = (id (dom ff)) | (dom g) by GRFUNC_1:23;
then g | SS = (id (dom ff)) | (SSS null (dom g)) by RELAT_1:71;
then B0: g .: SS = (id (dom ff)) .: SS
.= SomePoints ff ;
g | OO = ((id (dom ff)) | (dom g)) | OO by GRFUNC_1:23;
then g | OO = (id (dom ff)) | (OOO null (dom g)) by RELAT_1:71;
then B1: g .: OO = (id (dom ff)) .: OO
.= OtherPoints ff ;
ff .: (ff .: (SomePoints ff)) c= ff .: (OtherPoints ff) by Lm23, RELAT_1:123;
then ( SomePoints ff c= ff .: (OtherPoints ff) & ff .: (OtherPoints ff) c= SomePoints ff ) by B0, Lm24, RELAT_1:126;
hence f .: (OtherPoints f) = SomePoints f by XBOOLE_0:def 10; :: thesis: f .: (SomePoints f) = OtherPoints f
ff .: (ff .: (OtherPoints ff)) c= ff .: (SomePoints ff) by Lm24, RELAT_1:123;
then ( OtherPoints ff c= ff .: (SomePoints ff) & ff .: (SomePoints ff) c= OtherPoints ff ) by B1, Lm23, RELAT_1:126;
hence f .: (SomePoints f) = OtherPoints f by XBOOLE_0:def 10; :: thesis: verum