Suppose that

 fix = λf.(λx.f (x x)) (λx.f (x x)).

Show that, for every F, fix F = F(fix F).

In each term, a redex (λv.A) B that is about to be replaced is shown with the λ in green, the function body in red and the argument in blue.

An expression that is about to be replaced with an equal expression is shown in purple.

1. fix F
   
    = λf.(λx.f (x x)) (λx.f (x x)) F
   
    ⇒_β (λx.F(x x)) (λx.F(x x))
   
   

2. (λx.F(x x)) (λx.F(x x))
   
    ⇒_β F((λx.F(x x)) (λx.F(x x)))
   
   

3. F((λx.F(x x)) (λx.F(x x)))
   
    = F(fix F) (by (a))