let C be category; :: thesis: AllIso (AllIso C) = AllIso C
A1:
the carrier of (AllIso (AllIso C)) = the carrier of (AllIso C)
by Def5;
A2:
the carrier of (AllIso C) = the carrier of C
by Def5;
A3:
the Arrows of (AllIso (AllIso C)) cc= the Arrows of (AllIso C)
by Def5;
now let i be
set ;
:: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of (AllIso (AllIso C)) . i = the Arrows of (AllIso C) . i )assume A4:
i in [:the carrier of C,the carrier of C:]
;
:: thesis: the Arrows of (AllIso (AllIso C)) . i = the Arrows of (AllIso 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
(AllIso C) by A5, Def5;
thus
the
Arrows of
(AllIso (AllIso C)) . i = the
Arrows of
(AllIso C) . i
:: thesis: verumproof
thus
the
Arrows of
(AllIso (AllIso C)) . i c= the
Arrows of
(AllIso C) . i
by A1, A2, A3, A4, ALTCAT_2:def 2;
:: according to XBOOLE_0:def 10 :: thesis: the Arrows of (AllIso C) . i c= the Arrows of (AllIso (AllIso C)) . i
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllIso C) . i or n in the Arrows of (AllIso (AllIso C)) . i )
assume A6:
n in the
Arrows of
(AllIso C) . i
;
:: thesis: n in the Arrows of (AllIso (AllIso C)) . i
then reconsider n1 =
n as
Morphism of
o1,
o2 by A5;
A7:
n1 " in <^o2,o1^>
by A5, A6, Th52;
n1 is
iso
by A5, A6, Th52;
then
n in the
Arrows of
(AllIso (AllIso C)) . o1,
o2
by A5, A6, A7, Def5;
hence
n in the
Arrows of
(AllIso (AllIso C)) . i
by A5;
:: thesis: verum
end; end;
hence
AllIso (AllIso C) = AllIso C
by A1, A2, ALTCAT_2:26, PBOOLE:3; :: thesis: verum