let C be category; :: thesis: AllMono (AllMono C) = AllMono C
A1:
the carrier of (AllMono (AllMono C)) = the carrier of (AllMono C)
by Def1;
A2:
the carrier of (AllMono C) = the carrier of C
by Def1;
A3:
the Arrows of (AllMono (AllMono C)) cc= the Arrows of (AllMono C)
by Def1;
now let i be
set ;
:: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of (AllMono (AllMono C)) . i = the Arrows of (AllMono C) . i )assume A4:
i in [:the carrier of C,the carrier of C:]
;
:: thesis: the Arrows of (AllMono (AllMono C)) . i = the Arrows of (AllMono C) . ithen consider o1,
o2 being
set such that A5:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C &
i = [o1,o2] )
by ZFMISC_1:103;
reconsider o1 =
o1,
o2 =
o2 as
object of
(AllMono C) by A5, Def1;
thus
the
Arrows of
(AllMono (AllMono C)) . i = the
Arrows of
(AllMono C) . i
:: thesis: verumproof
thus
the
Arrows of
(AllMono (AllMono C)) . i c= the
Arrows of
(AllMono C) . i
by A1, A2, A3, A4, ALTCAT_2:def 2;
:: according to XBOOLE_0:def 10 :: thesis: the Arrows of (AllMono C) . i c= the Arrows of (AllMono (AllMono C)) . i
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllMono C) . i or n in the Arrows of (AllMono (AllMono C)) . i )
assume A6:
n in the
Arrows of
(AllMono C) . i
;
:: thesis: n in the Arrows of (AllMono (AllMono C)) . i
then reconsider n1 =
n as
Morphism of
o1,
o2 by A5;
n1 is
mono
by A5, A6, Th50;
then
n in the
Arrows of
(AllMono (AllMono C)) . o1,
o2
by A5, A6, Def1;
hence
n in the
Arrows of
(AllMono (AllMono C)) . i
by A5;
:: thesis: verum
end; end;
hence
AllMono (AllMono C) = AllMono C
by A1, A2, ALTCAT_2:26, PBOOLE:3; :: thesis: verum