let A be non empty AltCatStr ; for B being non empty SubCatStr of A holds
( B is full iff incl B is full )
let B be non empty SubCatStr of A; ( B is full iff incl B is full )
hereby ( incl B is full implies B is full )
ex
I29 being non
empty set ex
B9 being
ManySortedSet of
I29 ex
f9 being
Function of
[: the carrier of B, the carrier of B:],
I29 st
( the
ObjectMap of
(incl B) = f9 & the
Arrows of
A = B9 & the
MorphMap of
(incl B) is
ManySortedFunction of the
Arrows of
B,
B9 * f9 )
by FUNCTOR0:def 3;
then reconsider f = the
MorphMap of
(incl B) as
ManySortedFunction of the
Arrows of
B, the
Arrows of
A * the
ObjectMap of
(incl B) ;
set I =
[: the carrier of B, the carrier of B:];
( the
carrier of
B c= the
carrier of
A &
dom the
Arrows of
A = [: the carrier of A, the carrier of A:] )
by ALTCAT_2:def 11, PARTFUN1:def 2;
then A1:
(dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:]
by XBOOLE_1:28, ZFMISC_1:96;
assume A2:
B is
full
;
incl B is full
f is
"onto"
hence
incl B is
full
;
verum
set I = [: the carrier of B, the carrier of B:];
A5:
the carrier of B c= the carrier of A
by ALTCAT_2:def 11;
then A6:
[: the carrier of B, the carrier of B:] c= [: the carrier of A, the carrier of A:]
by ZFMISC_1:96;
dom the Arrows of A = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;
then A7:
(dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:]
by A5, XBOOLE_1:28, ZFMISC_1:96;
then
dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) = [: the carrier of B, the carrier of B:]
by RELAT_1:61;
then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of [: the carrier of B, the carrier of B:] by PARTFUN1:def 2;
assume A8:
incl B is full
; B is full
A9:
XX c= the Arrows of B
proof
let i be
object ;
PBOOLE:def 2 ( not i in [: the carrier of B, the carrier of B:] or XX . i c= the Arrows of B . i )
assume A10:
i in [: the carrier of B, the carrier of B:]
;
XX . i c= the Arrows of B . i
let x be
object ;
TARSKI:def 3 ( not x in XX . i or x in the Arrows of B . i )
assume A11:
x in XX . i
;
x in the Arrows of B . i
x in the
Arrows of
B . i
proof
consider f being
ManySortedFunction of the
Arrows of
B, the
Arrows of
A * the
ObjectMap of
(incl B) such that A12:
f = the
MorphMap of
(incl B)
and A13:
f is
"onto"
by A8;
f = id the
Arrows of
B
by A12, FUNCTOR0:def 28;
then A14:
rng ((id the Arrows of B) . i) =
( the Arrows of A * the ObjectMap of (incl B)) . i
by A10, A13
.=
( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i
by FUNCTOR0:def 28
.=
the
Arrows of
A . i
by A7, A10, FUNCT_1:20
;
consider y,
z being
object such that
y in the
carrier of
A
and
z in the
carrier of
A
and A15:
i = [y,z]
by A6, A10, ZFMISC_1:84;
(
y in the
carrier of
B &
z in the
carrier of
B )
by A10, A15, ZFMISC_1:87;
then A16:
XX . (
y,
z)
= the
Arrows of
A . (
y,
z)
by A5, ALTCAT_1:5;
rng ((id the Arrows of B) . i) =
rng (id ( the Arrows of B . i))
by A10, MSUALG_3:def 1
.=
the
Arrows of
B . i
;
hence
x in the
Arrows of
B . i
by A11, A15, A16, A14;
verum
end;
hence
x in the
Arrows of
B . i
;
verum
end;
the Arrows of B c= XX
proof
let i be
object ;
PBOOLE:def 2 ( not i in [: the carrier of B, the carrier of B:] or the Arrows of B . i c= XX . i )
assume A17:
i in [: the carrier of B, the carrier of B:]
;
the Arrows of B . i c= XX . i
then consider y,
z being
object such that
y in the
carrier of
A
and
z in the
carrier of
A
and A18:
i = [y,z]
by A6, ZFMISC_1:84;
(
y in the
carrier of
B &
z in the
carrier of
B )
by A17, A18, ZFMISC_1:87;
then A19:
XX . (
y,
z)
= the
Arrows of
A . (
y,
z)
by A5, ALTCAT_1:5;
let x be
object ;
TARSKI:def 3 ( not x in the Arrows of B . i or x in XX . i )
assume A20:
x in the
Arrows of
B . i
;
x in XX . i
the
Arrows of
B cc= the
Arrows of
A
by ALTCAT_2:def 11;
then
the
Arrows of
B . (
y,
z)
c= the
Arrows of
A . (
y,
z)
by A17, A18;
hence
x in XX . i
by A18, A20, A19;
verum
end;
hence
the Arrows of B = the Arrows of A || the carrier of B
by A9, PBOOLE:146; ALTCAT_2:def 13 verum