reconsider N = n as Element of NAT by ORDINAL1:def 12;
the homogeneous Function of (TOP-REAL N),(TOP-REAL N) is homogeneous ;
hence ex b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ is homogeneous ; :: thesis: verum