let g be Function; :: thesis: ( (rng g) \ (dom g) = {} & g is involutive & (field g) \ (fixpoints g) <> {} implies ( SomePoints g <> {} & OtherPoints g <> {} ) )

assume (rng g) \ (dom g) = {} ; :: thesis: ( not g is involutive or not (field g) \ (fixpoints g) <> {} or ( SomePoints g <> {} & OtherPoints g <> {} ) )

then B0: rng g c= dom g by FOMODEL0:29;

assume B1: ( g is involutive & (field g) \ (fixpoints g) <> {} ) ; :: thesis: ( SomePoints g <> {} & OtherPoints g <> {} )

hence SomePoints g <> {} by Lm25, B0; :: thesis: OtherPoints g <> {}

then g .: (OtherPoints g) <> {} by Lm30, B0, B1;

hence OtherPoints g <> {} ; :: thesis: verum

assume (rng g) \ (dom g) = {} ; :: thesis: ( not g is involutive or not (field g) \ (fixpoints g) <> {} or ( SomePoints g <> {} & OtherPoints g <> {} ) )

then B0: rng g c= dom g by FOMODEL0:29;

assume B1: ( g is involutive & (field g) \ (fixpoints g) <> {} ) ; :: thesis: ( SomePoints g <> {} & OtherPoints g <> {} )

hence SomePoints g <> {} by Lm25, B0; :: thesis: OtherPoints g <> {}

then g .: (OtherPoints g) <> {} by Lm30, B0, B1;

hence OtherPoints g <> {} ; :: thesis: verum