We will prove ∃f : set, continuous_map unit_interval unit_interval_topology unit_square unit_square_topology f.
The rest of this subproof is missing.
∎