let C be category; :: thesis: AllEpi (AllEpi C) = AllEpi C

A1: ( the carrier of (AllEpi (AllEpi C)) = the carrier of (AllEpi C) & the carrier of (AllEpi C) = the carrier of C ) by Def2;

A2: the Arrows of (AllEpi (AllEpi C)) cc= the Arrows of (AllEpi C) by Def2;

A1: ( the carrier of (AllEpi (AllEpi C)) = the carrier of (AllEpi C) & the carrier of (AllEpi C) = the carrier of C ) by Def2;

A2: the Arrows of (AllEpi (AllEpi C)) cc= the Arrows of (AllEpi C) by Def2;

now :: thesis: for i being object st i in [: the carrier of C, the carrier of C:] holds

the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i

hence
AllEpi (AllEpi C) = AllEpi C
by A1, ALTCAT_2:25, PBOOLE:3; :: thesis: verumthe Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i

let i be object ; :: thesis: ( i in [: the carrier of C, the carrier of C:] implies the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i )

assume A3: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i

then consider o1, o2 being object 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 (AllEpi C) by A4, Def2;

thus the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i :: thesis: verum

end;assume A3: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i

then consider o1, o2 being object 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 (AllEpi C) by A4, Def2;

thus the Arrows of (AllEpi (AllEpi C)) . i = the Arrows of (AllEpi C) . i :: thesis: verum

proof

thus
the Arrows of (AllEpi (AllEpi C)) . i c= the Arrows of (AllEpi C) . i
by A1, A2, A3; :: according to XBOOLE_0:def 10 :: thesis: the Arrows of (AllEpi C) . i c= the Arrows of (AllEpi (AllEpi C)) . i

let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllEpi C) . i or n in the Arrows of (AllEpi (AllEpi C)) . i )

assume A6: n in the Arrows of (AllEpi C) . i ; :: thesis: n in the Arrows of (AllEpi (AllEpi C)) . i

then reconsider n1 = n as Morphism of o1,o2 by A5;

n1 is epi by A5, A6, Th51;

then n in the Arrows of (AllEpi (AllEpi C)) . (o1,o2) by A5, A6, Def2;

hence n in the Arrows of (AllEpi (AllEpi C)) . i by A5; :: thesis: verum

end;let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of (AllEpi C) . i or n in the Arrows of (AllEpi (AllEpi C)) . i )

assume A6: n in the Arrows of (AllEpi C) . i ; :: thesis: n in the Arrows of (AllEpi (AllEpi C)) . i

then reconsider n1 = n as Morphism of o1,o2 by A5;

n1 is epi by A5, A6, Th51;

then n in the Arrows of (AllEpi (AllEpi C)) . (o1,o2) by A5, A6, Def2;

hence n in the Arrows of (AllEpi (AllEpi C)) . i by A5; :: thesis: verum