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 4;
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 4;
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:119;
assume A2:
B is
full
;
incl B is full
f is
"onto"
hence
incl B is
full
by FUNCTOR0:def 33;
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:119;
dom the Arrows of A = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 4;
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:119;
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:90;
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 4;
assume A8:
incl B is full
; B is full
A9:
XX c= the Arrows of B
proof
let i be
set ;
PBOOLE:def 5 ( 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
set ;
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, FUNCTOR0:def 33;
f = id the
Arrows of
B
by A12, FUNCTOR0:def 29;
then A14:
rng ((id the Arrows of B) . i) =
(the Arrows of A * the ObjectMap of (incl B)) . i
by A10, A13, MSUALG_3:def 3
.=
(the Arrows of A * (id [:the carrier of B,the carrier of B:])) . i
by FUNCTOR0:def 29
.=
the
Arrows of
A . i
by A7, A10, FUNCT_1:38
;
consider y,
z being
set 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:103;
(
y in the
carrier of
B &
z in the
carrier of
B )
by A10, A15, ZFMISC_1:106;
then A16:
XX . y,
z = the
Arrows of
A . y,
z
by A5, ALTCAT_1:7;
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
by RELAT_1:71
;
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
set ;
PBOOLE:def 5 ( 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
set such that
y in the
carrier of
A
and
z in the
carrier of
A
and A18:
i = [y,z]
by A6, ZFMISC_1:103;
(
y in the
carrier of
B &
z in the
carrier of
B )
by A17, A18, ZFMISC_1:106;
then A19:
XX . y,
z = the
Arrows of
A . y,
z
by A5, ALTCAT_1:7;
let x be
set ;
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, ALTCAT_2:def 2;
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:def 13; ALTCAT_2:def 13 verum