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 ;
PBOOLE:def 15 ( 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}:]
;
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;
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
;
ALTCAT_2:def 11 ( 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
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:]
;
ALTCAT_2:def 2 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 ;
( 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 #):]
;
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;
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:]
;
ALTCAT_2:def 2 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 ;
( 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 #):]
;
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
;
verum
end;
then reconsider D = AltCatStr(# {o},a,m #) as strict SubCatStr of C ;
take
D
; ( 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)) )
; verum