theorem :: ZF_FUND1:28

( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega ) by Lm1;