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, PARTFUN1, CARD_3, MSUALG_6, MSAFREE, TARSKI, MCART_1, ALTCAT_6;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, ORDINAL1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, FUNCOP_1, STRUCT_0, ALTCAT_1, ALTCAT_3, ALTCAT_5, MSAFREE;
definitions TARSKI, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, FUNCT_2, ALTCAT_3;
theorems FUNCT_2, FUNCOP_1, TARSKI, ALTCAT_1, FUNCT_5, FUNCT_1, ALTCAT_3, PARTFUN1, MSAFREE, XTUPLE_0, XBOOLE_0, SCMYCIEL, CARD_3, SUBSET_1;
schemes PBOOLE, FUNCT_2, CLASSES1;
registrations XBOOLE_0, RELSET_1, FUNCOP_1, STRUCT_0, ALTCAT_1, FUNCT_2, FUNCT_1, RELAT_1, ALTCAT_5, MSAFREE, XTUPLE_0;
constructors HIDDEN, ALTCAT_3, RELSET_1, ALTCAT_5, MSAFREE;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, ORDINAL1, CARD_3;
expansions PARTFUN1;
set C = EnsCat {{}};
Lm1:
the carrier of (EnsCat {{}}) = {0}
by ALTCAT_1:def 14;
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;