let C be category; :: thesis: AllIso (AllIso C) = AllIso C
A1: ( the carrier of (AllIso (AllIso C)) = the carrier of (AllIso C) & the carrier of (AllIso C) = the carrier of C ) by Def5;
A2: 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 A3: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of (AllIso (AllIso C)) . i = the Arrows of (AllIso C) . i
then consider o1, o2 being set such that
A4: ( o1 in the carrier of C & o2 in the carrier of C ) and
A5: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as object of (AllIso C) by A4, Def5;
thus the Arrows of (AllIso (AllIso C)) . i = the Arrows of (AllIso C) . i :: thesis: verum

proof

thus the Arrows of (AllIso (AllIso C)) . i c= the Arrows of (AllIso C) . i by A1, A2, A3, 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;
( n1 " in <^o2,o1^> & n1 is iso ) by A5, A6, Th52;
then n in the Arrows of (AllIso (AllIso C)) . (o1,o2) by A5, A6, 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, ALTCAT_2:25, PBOOLE:3; :: thesis: verum