let C be category; :: thesis: ( ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds m is mono ) implies AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllMono C )
assume A1: for o1, o2 being object of C
for m being Morphism of o1,o2 holds m is mono ; :: thesis: AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllMono C
A2: the carrier of (AllMono C) = the carrier of AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) by Def1;
A3: the Arrows of (AllMono C) cc= the Arrows of C by Def1;

now

let i be set ; :: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of (AllMono C) . i = the Arrows of C . i )
assume A4: i in [:the carrier of C,the carrier of C:] ; :: thesis: the Arrows of (AllMono C) . i = the Arrows of C . i
then 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 C by A5;
thus the Arrows of (AllMono C) . i = the Arrows of C . i :: thesis: verum

proof

thus the Arrows of (AllMono C) . i c= the Arrows of C . i by A2, A3, A4, ALTCAT_2:def 2; :: according to XBOOLE_0:def 10 :: thesis: the Arrows of C . i c= the Arrows of (AllMono C) . i
let n be set ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of C . i or n in the Arrows of (AllMono C) . i )
assume A6: n in the Arrows of C . i ; :: thesis: n in the Arrows of (AllMono C) . i
then reconsider n1 = n as Morphism of o1,o2 by A5;
n1 is mono by A1;
then n in the Arrows of (AllMono C) . o1,o2 by A5, A6, Def1;
hence n in the Arrows of (AllMono C) . i by A5; :: thesis: verum

end;

end;

hence AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllMono C by A2, ALTCAT_2:26, PBOOLE:3; :: thesis: verum