environ
vocabularies HIDDEN, ALTCAT_1, CAT_1, RELAT_1, ALTCAT_3, CAT_3, FUNCT_1, PBOOLE, ALTCAT_5, FUNCOP_1, CARD_1, FUNCT_2, XBOOLE_0, SUBSET_1, STRUCT_0, TARSKI, PARTFUN1, CARD_3, MSUALG_6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, FUNCOP_1, NUMBERS, STRUCT_0, ALTCAT_1, ALTCAT_3;
definitions TARSKI, RELAT_1, FUNCOP_1, PARTFUN1, ALTCAT_3;
theorems FUNCT_2, FUNCOP_1, CARD_1, TARSKI, ALTCAT_1, FUNCT_5, FUNCT_1, ALTCAT_3, PARTFUN1, YELLOW17, RELAT_1, CARD_3, PBOOLE;
schemes PBOOLE, CLASSES1;
registrations XBOOLE_0, RELSET_1, FUNCOP_1, STRUCT_0, ALTCAT_1, FUNCT_2, FUNCT_1, CARD_3, RELAT_1;
constructors HIDDEN, ALTCAT_3, RELSET_1, CARD_3, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ALTCAT_1, ORDINAL1;
expansions PARTFUN1;
reconsider a = 0 , b = 1 as Element of 2 by CARD_1:50, TARSKI:def 2;
set C = EnsCat {{}};
Lm1:
the carrier of (EnsCat {{}}) = {0}
by ALTCAT_1:def 14;
reconsider o = {} as Object of (EnsCat {{}}) by Lm1, TARSKI:def 1;
Lm2:
Funcs ({},{}) = {{}}
by FUNCT_5:57;
Lm3:
now for o1, o being Object of (EnsCat {{}}) holds
( {} is Morphism of o1,o & {} in <^o1,o^> )
let o1,
o be
Object of
(EnsCat {{}});
( {} is Morphism of o1,o & {} in <^o1,o^> )A1:
(
o1 = {} &
o = {} )
by Lm1, TARSKI:def 1;
<^o1,o^> = Funcs (
o1,
o)
by ALTCAT_1:def 14;
hence
(
{} is
Morphism of
o1,
o &
{} in <^o1,o^> )
by A1, Lm1, Lm2;
verum
end;