let f be Function; :: thesis: ( f is involutive implies f .: () c= SomePoints f )
set F = FieldCover f;
set S = SomePoints f;
set O = OtherPoints f;
set ch = ChoiceOn ();
set A = field f;
set FP = fixpoints f;
set E = ;
assume B5: f is involutive ; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: () or y in SomePoints f )
assume B7: y in f .: () ; :: thesis:
then consider x being object such that
B0: ( x in dom f & x in OtherPoints f & y = f . x ) by FUNCT_1:def 6;
reconsider xx = x as set by TARSKI:1;
(f .: ()) \ (rng f) = {} ;
then ( f .: () c= rng f & (rng f) null (dom f) c= field f ) by FOMODEL0:29;
then B8: y in field f by ;
(OtherPoints f) \+\ ((() \ ()) /\ (rng ())) = {} ;
then B66: x in (() \ ()) /\ (rng ()) by ;
consider X1 being object such that
B1: ( X1 in dom () & x = () . X1 ) by ;
X1 in () \ by ;
then X1 in FieldCover f ;
then consider x1 being Element of dom f such that
B2: ( X1 = {x1,(f . x1)} & x1 in dom f ) ;
B3: {x,(f . x)} = {x1,(f . x1)} by ;
( f . x in rng () implies x in fixpoints f )
proof
assume f . x in rng () ; :: thesis:
then consider X2 being object such that
C0: ( X2 in dom () & f . x = () . X2 ) by FUNCT_1:def 3;
reconsider X22 = X2 as set by TARSKI:1;
X2 in () \ by ;
then X2 in FieldCover f ;
then consider x2 being Element of dom f such that
C1: ( X2 = {x2,(f . x2)} & x2 in dom f ) ;
f . x in X22 by ;
then (ChoiceOn ()) . X1 = () . X2 by ;
then xx is_a_fixpoint_of f by ;
hence x in fixpoints f by FOMODEL0:69; :: thesis: verum
end;
hence y in SomePoints f by ; :: thesis: verum