let C be category; :: thesis: ( ( for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m is retraction & <^o2,o1^> <> {} ) ) implies AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C )

assume A1: for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m is retraction & <^o2,o1^> <> {} ) ; :: thesis: AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C

A2: the carrier of (AllRetr C) = the carrier of AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Def3;

A3: the Arrows of (AllRetr C) cc= the Arrows of C by Def3;

for m being Morphism of o1,o2 holds

( m is retraction & <^o2,o1^> <> {} ) ) implies AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C )

assume A1: for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m is retraction & <^o2,o1^> <> {} ) ; :: thesis: AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C

A2: the carrier of (AllRetr C) = the carrier of AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Def3;

A3: the Arrows of (AllRetr C) cc= the Arrows of C by Def3;

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

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

hence
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C
by A2, ALTCAT_2:25, PBOOLE:3; :: thesis: verumthe Arrows of (AllRetr C) . i = the Arrows of C . i

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

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

then consider o1, o2 being object such that

A5: ( o1 in the carrier of C & o2 in the carrier of C ) and

A6: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A5;

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

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

then consider o1, o2 being object such that

A5: ( o1 in the carrier of C & o2 in the carrier of C ) and

A6: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A5;

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

proof

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

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

assume A7: n in the Arrows of C . i ; :: thesis: n in the Arrows of (AllRetr C) . i

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

( <^o2,o1^> <> {} & n1 is retraction ) by A1;

then n in the Arrows of (AllRetr C) . (o1,o2) by A6, A7, Def3;

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

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

assume A7: n in the Arrows of C . i ; :: thesis: n in the Arrows of (AllRetr C) . i

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

( <^o2,o1^> <> {} & n1 is retraction ) by A1;

then n in the Arrows of (AllRetr C) . (o1,o2) by A6, A7, Def3;

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