let C be non empty transitive AltCatStr ; :: thesis:
let D be non empty transitive SubCatStr of C; :: thesis:
let o1, o2 be Object of C; :: thesis:
let p1, p2 be Object of D; :: thesis:
let m be Morphism of o1,o2; :: thesis:
let n be Morphism of p1,p2; :: thesis:
assume that
A1: p1 = o1 and
A2: p2 = o2 and
A3: ( m = n & <^p1,p2^> <> {} ) ; :: thesis:
thus ( m is mono implies n is mono ) :: thesis:

proof

assume A4: m is mono ; :: thesis:
let p3 be Object of D; :: according to ALTCAT_3:def 7 :: thesis:
assume A5: <^p3,p1^> <> {} ; :: thesis:
reconsider o3 = p3 as Object of C by ALTCAT_2:29;
A6: <^o3,o1^> <> {} by A1, A5, ALTCAT_2:31, XBOOLE_1:3;
let f, g be Morphism of p3,p1; :: thesis:
assume A7: n * f = n * g ; :: thesis:
reconsider f1 = f, g1 = g as Morphism of o3,o1 by A1, A5, ALTCAT_2:33;
m * f1 = n * f by A1, A2, A3, A5, ALTCAT_2:32
.= m * g1 by A1, A2, A3, A5, A7, ALTCAT_2:32 ;
hence f = g by A4, A6; :: thesis:

end;

assume A8: m is epi ; :: thesis:
let p3 be Object of D; :: according to ALTCAT_3:def 8 :: thesis:
assume A9: <^p2,p3^> <> {} ; :: thesis:
reconsider o3 = p3 as Object of C by ALTCAT_2:29;
A10: <^o2,o3^> <> {} by A2, A9, ALTCAT_2:31, XBOOLE_1:3;
let f, g be Morphism of p2,p3; :: thesis:
assume A11: f * n = g * n ; :: thesis:
reconsider f1 = f, g1 = g as Morphism of o2,o3 by A2, A9, ALTCAT_2:33;
f1 * m = f * n by A1, A2, A3, A9, ALTCAT_2:32
.= g1 * m by A1, A2, A3, A9, A11, ALTCAT_2:32 ;
hence f = g by A8, A10; :: thesis: