Apply df_cart__df_img__df_domain__df_range__df_cup__df_cap__df_restrict__df_succf__df_apply__df_funpart__df_fullfun__df_ub__df_lb__df_altop__df_altxp__df_ofs__df_transport__df_colinear with wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))).

Assume H0: wceq ccart (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cpprod cep cep) cvv)))).

Assume H1: wceq cimg (ccom (cimage (cres (ccom c2nd c1st) (cres c1st (cxp cvv cvv)))) ccart).

Assume H2: wceq cdomain (cimage (cres c1st (cxp cvv cvv))).

Assume H3: wceq crange (cimage (cres c2nd (cxp cvv cvv))).

Assume H4: wceq ccup (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cun (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))).

Assume H5: wceq ccap (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cin (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))).

Assume H6: wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))).

Assume H7: wceq csuccf (ccom ccup (ctxp cid csingle)).

Assume H8: wceq capply (ccom (ccom cbigcup cbigcup) (ccom (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cres cep csingles) cvv)))) (ccom (ccom csingle cimg) (cpprod cid csingle)))).

Assume H9: ∀ x0 : ι → ο . wceq (cfunpart x0) (cres x0 (cdm (cin (ccom (cimage x0) csingle) (cxp cvv csingles)))).

Assume H10: ∀ x0 : ι → ο . wceq (cfullfn x0) (cun (cfunpart x0) (cxp (cdif cvv (cdm (cfunpart x0))) (csn c0))).

Assume H11: ∀ x0 : ι → ο . wceq (cub x0) (cdif (cxp cvv cvv) (ccom (cdif cvv x0) (ccnv cep))).

Assume H12: ∀ x0 : ι → ο . wceq (clb x0) (cub (ccnv x0)).

Assume H13: ∀ x0 x1 : ι → ο . wceq (caltop x0 x1) (cpr (csn x0) (cpr x0 (csn x1))).

Assume H14: ∀ x0 x1 : ι → ο . wceq (caltxp x0 x1) (cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (caltop (cv x3) (cv x4))) (λ x4 . x1)) (λ x3 . x0))).

...

■

Proofgold Proof