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]}
.= [:{o},{o},{o}:] by MCART_1:35 ;
then reconsider m = [o,o,o] .--> ( the Comp of C . (o,o,o)) as ManySortedSet of [:{o},{o},{o}:] ;
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 [:{o},{o}:] ;
A1: a . (o,o) = the Arrows of C . (o,o) by FUNCT_4:80;
m is ManySortedFunction of {|a,a|},{|a|}

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in [:{o},{o},{o}:] or m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] )
A2: o in {o} by TARSKI:def 1;
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:35;
then A3: i = [o,o,o] by TARSKI:def 1;
then A4: {|a|} . i = {|a|} . (o,o,o) by MULTOP_1:def 1
.= the Arrows of C . (o,o) by A1, A2, ALTCAT_1:def 3 ;
{|a,a|} . i = {|a,a|} . (o,o,o) by A3, MULTOP_1:def 1
.= [:( the Arrows of C . (o,o)),( the Arrows of C . (o,o)):] by A1, A2, ALTCAT_1:def 4 ;
hence m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] by A3, A4, FUNCOP_1:72; :: 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 C

proof

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:29;
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:35;
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:72
.= 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