set a = o,o :-> <^o,o^>;
dom (o,o :-> <^o,o^>) = [:{o},{o}:]
by FUNCT_2:def 1;
then reconsider a = o,o :-> <^o,o^> as ManySortedSet of by PARTFUN1:def 4;
set m = [o,o,o] .--> (the Comp of C . o,o,o);
dom ([o,o,o] .--> (the Comp of C . o,o,o)) =
{[o,o,o]}
by FUNCOP_1:19
.=
[:{o},{o},{o}:]
by MCART_1:39
;
then reconsider m = [o,o,o] .--> (the Comp of C . o,o,o) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A1:
a . o,o = the Arrows of C . o,o
by ALTCAT_1:12;
m is ManySortedFunction of {|a,a|},{|a|}
proof
let i be
set ;
:: according to PBOOLE:def 18 :: thesis: ( not i in [:{o},{o},{o}:] or m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] )
assume
i in [:{o},{o},{o}:]
;
:: thesis: m . i is Element of bool [:({|a,a|} . i),({|a|} . i):]
then
i in {[o,o,o]}
by MCART_1:39;
then A2:
i = [o,o,o]
by TARSKI:def 1;
A3:
o in {o}
by TARSKI:def 1;
A4:
{|a,a|} . i =
{|a,a|} . o,
o,
o
by A2, MULTOP_1:def 1
.=
[:(the Arrows of C . o,o),(the Arrows of C . o,o):]
by A1, A3, ALTCAT_1:def 6
;
{|a|} . i =
{|a|} . o,
o,
o
by A2, MULTOP_1:def 1
.=
the
Arrows of
C . o,
o
by A1, A3, ALTCAT_1:def 5
;
hence
m . i is
Element of
bool [:({|a,a|} . i),({|a|} . i):]
by A2, A4, FUNCOP_1:87;
:: thesis: verum
end;
then reconsider m = m as BinComp of a ;
set D = AltCatStr(# {o},a,m #);
AltCatStr(# {o},a,m #) is SubCatStr of C
proof
thus
the
carrier of
AltCatStr(#
{o},
a,
m #)
c= the
carrier of
C
;
:: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of AltCatStr(# {o},a,m #) cc= the Arrows of C & the Comp of AltCatStr(# {o},a,m #) cc= the Comp of C )
thus
the
Arrows of
AltCatStr(#
{o},
a,
m #)
cc= the
Arrows of
C
:: thesis: the Comp of AltCatStr(# {o},a,m #) cc= the Comp of Cproof
thus
[:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] c= [:the carrier of C,the carrier of C:]
;
:: according to ALTCAT_2:def 2 :: thesis: for i being set st i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] holds
the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i
let i be
set ;
:: thesis: ( i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] implies the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i )
assume
i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):]
;
:: thesis: the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i
then
i in {[o,o]}
by ZFMISC_1:35;
then
i = [o,o]
by TARSKI:def 1;
hence
the
Arrows of
AltCatStr(#
{o},
a,
m #)
. i c= the
Arrows of
C . i
by A1;
:: thesis: verum
end;
thus
[:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] c= [:the carrier of C,the carrier of C,the carrier of C:]
;
:: according to ALTCAT_2:def 2 :: thesis: for i being set st i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] holds
the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i
let i be
set ;
:: thesis: ( i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):] implies the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i )
assume
i in [:the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #),the carrier of AltCatStr(# {o},a,m #):]
;
:: thesis: the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i
then
i in {[o,o,o]}
by MCART_1:39;
then A5:
i = [o,o,o]
by TARSKI:def 1;
then the
Comp of
AltCatStr(#
{o},
a,
m #)
. i =
the
Comp of
C . o,
o,
o
by FUNCOP_1:87
.=
the
Comp of
C . i
by A5, MULTOP_1:def 1
;
hence
the
Comp of
AltCatStr(#
{o},
a,
m #)
. i c= the
Comp of
C . i
;
:: thesis: verum
end;
then reconsider D = AltCatStr(# {o},a,m #) as strict SubCatStr of C ;
take
D
; :: thesis: ( the carrier of D = {o} & the Arrows of D = o,o :-> <^o,o^> & the Comp of D = [o,o,o] .--> (the Comp of C . o,o,o) )
thus
( the carrier of D = {o} & the Arrows of D = o,o :-> <^o,o^> & the Comp of D = [o,o,o] .--> (the Comp of C . o,o,o) )
; :: thesis: verum