710 thus ?thesis using inj_on_iff_surj[of B "B \<times> A"] |
687 thus ?thesis using inj_on_iff_surj[of B "B \<times> A"] |
711 card_of_ordLeq[of B "B \<times> A"] * by blast |
688 card_of_ordLeq[of B "B \<times> A"] * by blast |
712 qed |
689 qed |
713 |
690 |
714 |
691 |
|
692 lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|" |
|
693 proof- |
|
694 let ?f = "\<lambda>(a::'a,b::'b). (b,a)" |
|
695 have "bij_betw ?f (A \<times> B) (B \<times> A)" |
|
696 unfolding bij_betw_def inj_on_def by auto |
|
697 thus ?thesis using card_of_ordIso by blast |
|
698 qed |
|
699 |
|
700 |
|
701 lemma card_of_Times2: |
|
702 assumes "A \<noteq> {}" shows "|B| \<le>o |A \<times> B|" |
|
703 using assms card_of_Times1[of A B] card_of_Times_commute[of B A] |
|
704 ordLeq_ordIso_trans by blast |
|
705 |
|
706 |
715 corollary Card_order_Times1: |
707 corollary Card_order_Times1: |
716 "\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|" |
708 "\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|" |
717 using card_of_Times1[of B] card_of_Field_ordIso |
709 using card_of_Times1[of B] card_of_Field_ordIso |
718 ordIso_ordLeq_trans ordIso_symmetric by blast |
710 ordIso_ordLeq_trans ordIso_symmetric by blast |
719 |
|
720 |
|
721 lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|" |
|
722 proof- |
|
723 let ?f = "\<lambda>(a::'a,b::'b). (b,a)" |
|
724 have "bij_betw ?f (A \<times> B) (B \<times> A)" |
|
725 unfolding bij_betw_def inj_on_def by auto |
|
726 thus ?thesis using card_of_ordIso by blast |
|
727 qed |
|
728 |
|
729 |
|
730 lemma card_of_Times2: |
|
731 assumes "A \<noteq> {}" shows "|B| \<le>o |A \<times> B|" |
|
732 using assms card_of_Times1[of A B] card_of_Times_commute[of B A] |
|
733 ordLeq_ordIso_trans by blast |
|
734 |
711 |
735 |
712 |
736 corollary Card_order_Times2: |
713 corollary Card_order_Times2: |
737 "\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|" |
714 "\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|" |
738 using card_of_Times2[of A] card_of_Field_ordIso |
715 using card_of_Times2[of A] card_of_Field_ordIso |
1311 ordIso_transitive[of "|Field r <+> Field p|"] |
1255 ordIso_transitive[of "|Field r <+> Field p|"] |
1312 ordIso_transitive[of _ "|Field r|"] by blast |
1256 ordIso_transitive[of _ "|Field r|"] by blast |
1313 qed |
1257 qed |
1314 |
1258 |
1315 |
1259 |
1316 lemma card_of_Un_infinite: |
|
1317 assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|" |
|
1318 shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|" |
|
1319 proof- |
|
1320 have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq) |
|
1321 moreover have "|A <+> B| =o |A|" |
|
1322 using assms by (metis card_of_Plus_infinite) |
|
1323 ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast |
|
1324 hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast |
|
1325 thus ?thesis using Un_commute[of B A] by auto |
|
1326 qed |
|
1327 |
|
1328 |
|
1329 lemma card_of_Un_diff_infinite: |
|
1330 assumes INF: "infinite A" and LESS: "|B| <o |A|" |
|
1331 shows "|A - B| =o |A|" |
|
1332 proof- |
|
1333 obtain C where C_def: "C = A - B" by blast |
|
1334 have "|A \<union> B| =o |A|" |
|
1335 using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast |
|
1336 moreover have "C \<union> B = A \<union> B" unfolding C_def by auto |
|
1337 ultimately have 1: "|C \<union> B| =o |A|" by auto |
|
1338 (* *) |
|
1339 {assume *: "|C| \<le>o |B|" |
|
1340 moreover |
|
1341 {assume **: "finite B" |
|
1342 hence "finite C" |
|
1343 using card_of_ordLeq_finite * by blast |
|
1344 hence False using ** INF card_of_ordIso_finite 1 by blast |
|
1345 } |
|
1346 hence "infinite B" by auto |
|
1347 ultimately have False |
|
1348 using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis |
|
1349 } |
|
1350 hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast |
|
1351 {assume *: "finite C" |
|
1352 hence "finite B" using card_of_ordLeq_finite 2 by blast |
|
1353 hence False using * INF card_of_ordIso_finite 1 by blast |
|
1354 } |
|
1355 hence "infinite C" by auto |
|
1356 hence "|C| =o |A|" |
|
1357 using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis |
|
1358 thus ?thesis unfolding C_def . |
|
1359 qed |
|
1360 |
|
1361 |
|
1362 lemma card_of_Plus_ordLess_infinite: |
|
1363 assumes INF: "infinite C" and |
|
1364 LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|" |
|
1365 shows "|A <+> B| <o |C|" |
|
1366 proof(cases "A = {} \<or> B = {}") |
|
1367 assume Case1: "A = {} \<or> B = {}" |
|
1368 hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|" |
|
1369 using card_of_Plus_empty1 card_of_Plus_empty2 by blast |
|
1370 hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|" |
|
1371 using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast |
|
1372 thus ?thesis using LESS1 LESS2 |
|
1373 ordIso_ordLess_trans[of "|A <+> B|" "|A|"] |
|
1374 ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast |
|
1375 next |
|
1376 assume Case2: "\<not>(A = {} \<or> B = {})" |
|
1377 {assume *: "|C| \<le>o |A <+> B|" |
|
1378 hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast |
|
1379 hence 1: "infinite A \<or> infinite B" using finite_Plus by blast |
|
1380 {assume Case21: "|A| \<le>o |B|" |
|
1381 hence "infinite B" using 1 card_of_ordLeq_finite by blast |
|
1382 hence "|A <+> B| =o |B|" using Case2 Case21 |
|
1383 by (auto simp add: card_of_Plus_infinite) |
|
1384 hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1385 } |
|
1386 moreover |
|
1387 {assume Case22: "|B| \<le>o |A|" |
|
1388 hence "infinite A" using 1 card_of_ordLeq_finite by blast |
|
1389 hence "|A <+> B| =o |A|" using Case2 Case22 |
|
1390 by (auto simp add: card_of_Plus_infinite) |
|
1391 hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1392 } |
|
1393 ultimately have False using ordLeq_total card_of_Well_order[of A] |
|
1394 card_of_Well_order[of B] by blast |
|
1395 } |
|
1396 thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"] |
|
1397 card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto |
|
1398 qed |
|
1399 |
|
1400 |
|
1401 lemma card_of_Plus_ordLess_infinite_Field: |
|
1402 assumes INF: "infinite (Field r)" and r: "Card_order r" and |
|
1403 LESS1: "|A| <o r" and LESS2: "|B| <o r" |
|
1404 shows "|A <+> B| <o r" |
|
1405 proof- |
|
1406 let ?C = "Field r" |
|
1407 have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso |
|
1408 ordIso_symmetric by blast |
|
1409 hence "|A| <o |?C|" "|B| <o |?C|" |
|
1410 using LESS1 LESS2 ordLess_ordIso_trans by blast+ |
|
1411 hence "|A <+> B| <o |?C|" using INF |
|
1412 card_of_Plus_ordLess_infinite by blast |
|
1413 thus ?thesis using 1 ordLess_ordIso_trans by blast |
|
1414 qed |
|
1415 |
|
1416 |
|
1417 lemma infinite_card_of_insert: |
|
1418 assumes "infinite A" |
|
1419 shows "|insert a A| =o |A|" |
|
1420 proof- |
|
1421 have iA: "insert a A = A \<union> {a}" by simp |
|
1422 show ?thesis |
|
1423 using infinite_imp_bij_betw2[OF assms] unfolding iA |
|
1424 by (metis bij_betw_inv card_of_ordIso) |
|
1425 qed |
|
1426 |
|
1427 |
|
1428 subsection {* Cardinals versus lists *} |
|
1429 |
|
1430 |
|
1431 text{* The next is an auxiliary operator, which shall be used for inductive |
|
1432 proofs of facts concerning the cardinality of @{text "List"} : *} |
|
1433 |
|
1434 definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set" |
|
1435 where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}" |
|
1436 |
|
1437 |
|
1438 lemma lists_def2: "lists A = {l. set l \<le> A}" |
|
1439 using in_listsI by blast |
|
1440 |
|
1441 |
|
1442 lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)" |
|
1443 unfolding lists_def2 nlists_def by blast |
|
1444 |
|
1445 |
|
1446 lemma card_of_lists: "|A| \<le>o |lists A|" |
|
1447 proof- |
|
1448 let ?h = "\<lambda> a. [a]" |
|
1449 have "inj_on ?h A \<and> ?h ` A \<le> lists A" |
|
1450 unfolding inj_on_def lists_def2 by auto |
|
1451 thus ?thesis by (metis card_of_ordLeq) |
|
1452 qed |
|
1453 |
|
1454 |
|
1455 lemma nlists_0: "nlists A 0 = {[]}" |
|
1456 unfolding nlists_def by auto |
|
1457 |
|
1458 |
|
1459 lemma nlists_not_empty: |
|
1460 assumes "A \<noteq> {}" |
|
1461 shows "nlists A n \<noteq> {}" |
|
1462 proof(induct n, simp add: nlists_0) |
|
1463 fix n assume "nlists A n \<noteq> {}" |
|
1464 then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto |
|
1465 hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto |
|
1466 thus "nlists A (Suc n) \<noteq> {}" by auto |
|
1467 qed |
|
1468 |
|
1469 |
|
1470 lemma Nil_in_lists: "[] \<in> lists A" |
|
1471 unfolding lists_def2 by auto |
|
1472 |
|
1473 |
|
1474 lemma lists_not_empty: "lists A \<noteq> {}" |
|
1475 using Nil_in_lists by blast |
|
1476 |
|
1477 |
|
1478 lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|" |
|
1479 proof- |
|
1480 let ?B = "A \<times> (nlists A n)" let ?h = "\<lambda>(a,l). a # l" |
|
1481 have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)" |
|
1482 unfolding inj_on_def nlists_def by auto |
|
1483 moreover have "nlists A (Suc n) \<le> ?h ` ?B" |
|
1484 proof(auto) |
|
1485 fix l assume "l \<in> nlists A (Suc n)" |
|
1486 hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto |
|
1487 then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv) |
|
1488 hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto |
|
1489 thus "l \<in> ?h ` ?B" using 2 unfolding nlists_def by auto |
|
1490 qed |
|
1491 ultimately have "bij_betw ?h ?B (nlists A (Suc n))" |
|
1492 unfolding bij_betw_def by auto |
|
1493 thus ?thesis using card_of_ordIso ordIso_symmetric by blast |
|
1494 qed |
|
1495 |
|
1496 |
|
1497 lemma card_of_nlists_infinite: |
|
1498 assumes "infinite A" |
|
1499 shows "|nlists A n| \<le>o |A|" |
|
1500 proof(induct n) |
|
1501 have "A \<noteq> {}" using assms by auto |
|
1502 thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq) |
|
1503 next |
|
1504 fix n assume IH: "|nlists A n| \<le>o |A|" |
|
1505 have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|" |
|
1506 using card_of_nlists_Succ by blast |
|
1507 moreover |
|
1508 {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast |
|
1509 hence "|A \<times> (nlists A n)| =o |A|" |
|
1510 using assms IH by (auto simp add: card_of_Times_infinite) |
|
1511 } |
|
1512 ultimately show "|nlists A (Suc n)| \<le>o |A|" |
|
1513 using ordIso_transitive ordIso_iff_ordLeq by blast |
|
1514 qed |
|
1515 |
|
1516 |
|
1517 lemma card_of_lists_infinite: |
|
1518 assumes "infinite A" |
|
1519 shows "|lists A| =o |A|" |
|
1520 proof- |
|
1521 have "|lists A| \<le>o |A|" |
|
1522 using assms |
|
1523 by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite |
|
1524 infinite_iff_card_of_nat card_of_nlists_infinite) |
|
1525 thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast |
|
1526 qed |
|
1527 |
|
1528 |
|
1529 lemma Card_order_lists_infinite: |
|
1530 assumes "Card_order r" and "infinite(Field r)" |
|
1531 shows "|lists(Field r)| =o r" |
|
1532 using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast |
|
1533 |
|
1534 |
|
1535 |
|
1536 subsection {* The cardinal $\omega$ and the finite cardinals *} |
1260 subsection {* The cardinal $\omega$ and the finite cardinals *} |
1537 |
1261 |
1538 |
1262 |
1539 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict |
1263 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict |
1540 order relation on |
1264 order relation on |
2043 ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |" |
1754 ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |" |
2044 using ordIso_transitive by blast |
1755 using ordIso_transitive by blast |
2045 hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))" |
1756 hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))" |
2046 using card_of_ordIso_finite by blast |
1757 using card_of_ordIso_finite by blast |
2047 thus ?thesis by (simp only: card_of_cardSuc_finite) |
1758 thus ?thesis by (simp only: card_of_cardSuc_finite) |
|
1759 qed |
|
1760 |
|
1761 |
|
1762 lemma card_of_Plus_ordLess_infinite: |
|
1763 assumes INF: "infinite C" and |
|
1764 LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|" |
|
1765 shows "|A <+> B| <o |C|" |
|
1766 proof(cases "A = {} \<or> B = {}") |
|
1767 assume Case1: "A = {} \<or> B = {}" |
|
1768 hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|" |
|
1769 using card_of_Plus_empty1 card_of_Plus_empty2 by blast |
|
1770 hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|" |
|
1771 using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast |
|
1772 thus ?thesis using LESS1 LESS2 |
|
1773 ordIso_ordLess_trans[of "|A <+> B|" "|A|"] |
|
1774 ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast |
|
1775 next |
|
1776 assume Case2: "\<not>(A = {} \<or> B = {})" |
|
1777 {assume *: "|C| \<le>o |A <+> B|" |
|
1778 hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast |
|
1779 hence 1: "infinite A \<or> infinite B" using finite_Plus by blast |
|
1780 {assume Case21: "|A| \<le>o |B|" |
|
1781 hence "infinite B" using 1 card_of_ordLeq_finite by blast |
|
1782 hence "|A <+> B| =o |B|" using Case2 Case21 |
|
1783 by (auto simp add: card_of_Plus_infinite) |
|
1784 hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1785 } |
|
1786 moreover |
|
1787 {assume Case22: "|B| \<le>o |A|" |
|
1788 hence "infinite A" using 1 card_of_ordLeq_finite by blast |
|
1789 hence "|A <+> B| =o |A|" using Case2 Case22 |
|
1790 by (auto simp add: card_of_Plus_infinite) |
|
1791 hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1792 } |
|
1793 ultimately have False using ordLeq_total card_of_Well_order[of A] |
|
1794 card_of_Well_order[of B] by blast |
|
1795 } |
|
1796 thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"] |
|
1797 card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto |
|
1798 qed |
|
1799 |
|
1800 |
|
1801 lemma card_of_Plus_ordLess_infinite_Field: |
|
1802 assumes INF: "infinite (Field r)" and r: "Card_order r" and |
|
1803 LESS1: "|A| <o r" and LESS2: "|B| <o r" |
|
1804 shows "|A <+> B| <o r" |
|
1805 proof- |
|
1806 let ?C = "Field r" |
|
1807 have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso |
|
1808 ordIso_symmetric by blast |
|
1809 hence "|A| <o |?C|" "|B| <o |?C|" |
|
1810 using LESS1 LESS2 ordLess_ordIso_trans by blast+ |
|
1811 hence "|A <+> B| <o |?C|" using INF |
|
1812 card_of_Plus_ordLess_infinite by blast |
|
1813 thus ?thesis using 1 ordLess_ordIso_trans by blast |
2048 qed |
1814 qed |
2049 |
1815 |
2050 |
1816 |
2051 lemma card_of_Plus_ordLeq_infinite_Field: |
1817 lemma card_of_Plus_ordLeq_infinite_Field: |
2052 assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" |
1818 assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" |
2381 qed(unfold Func_def mem_Collect_eq F_def, auto) |
2142 qed(unfold Func_def mem_Collect_eq F_def, auto) |
2382 qed |
2143 qed |
2383 thus ?thesis unfolding card_of_ordIso[symmetric] by blast |
2144 thus ?thesis unfolding card_of_ordIso[symmetric] by blast |
2384 qed |
2145 qed |
2385 |
2146 |
2386 lemma card_of_Func_mono: |
|
2387 fixes A1 A2 :: "'a set" and B :: "'b set" |
|
2388 assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}" |
|
2389 shows "|Func A1 B| \<le>o |Func A2 B|" |
|
2390 proof- |
|
2391 obtain bb where bb: "bb \<in> B" using B by auto |
|
2392 def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b) a. if a \<in> A2 then (if a \<in> A1 then f1 a else bb) |
|
2393 else undefined" |
|
2394 show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI) |
|
2395 show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe |
|
2396 fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g" |
|
2397 show "f = g" |
|
2398 proof(rule ext) |
|
2399 fix a show "f a = g a" |
|
2400 proof(cases "a \<in> A1") |
|
2401 case True |
|
2402 thus ?thesis using eq A12 unfolding F_def fun_eq_iff |
|
2403 by (elim allE[of _ a]) auto |
|
2404 qed(insert f g, unfold Func_def, fastforce) |
|
2405 qed |
|
2406 qed |
|
2407 qed(insert bb, unfold Func_def F_def, force) |
|
2408 qed |
|
2409 |
|
2410 lemma ordLeq_Func: |
|
2411 assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2" |
|
2412 shows "|A| \<le>o |Func A B|" |
|
2413 unfolding card_of_ordLeq[symmetric] proof(intro exI conjI) |
|
2414 let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined" |
|
2415 show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto |
|
2416 show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto |
|
2417 qed |
|
2418 |
|
2419 lemma infinite_Func: |
|
2420 assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2" |
|
2421 shows "infinite (Func A B)" |
|
2422 using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite) |
|
2423 |
|
2424 lemma card_of_Func_UNIV: |
2147 lemma card_of_Func_UNIV: |
2425 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|" |
2148 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|" |
2426 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI) |
2149 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI) |
2427 let ?F = "\<lambda> f (a::'a). ((f a)::'b)" |
2150 let ?F = "\<lambda> f (a::'a). ((f a)::'b)" |
2428 show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)" |
2151 show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)" |