let C be non empty transitive AltCatStr ; :: thesis: for D being non empty transitive SubCatStr of C

for o1, o2 being Object of C

for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let D be non empty transitive SubCatStr of C; :: thesis: for o1, o2 being Object of C

for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let o1, o2 be Object of C; :: thesis: for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let p1, p2 be Object of D; :: thesis: for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let m be Morphism of o1,o2; :: thesis: for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let n be Morphism of p1,p2; :: thesis: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} implies ( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) ) )

assume that

A1: p1 = o1 and

A2: p2 = o2 and

A3: ( m = n & <^p1,p2^> <> {} ) ; :: thesis: ( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

thus ( m is mono implies n is mono ) :: thesis: ( m is epi implies n is epi )

let p3 be Object of D; :: according to ALTCAT_3:def 8 :: thesis: ( <^p2,p3^> = {} or for b_{1}, b_{2} being M3(<^p2,p3^>) holds

( not b_{1} * n = b_{2} * n or b_{1} = b_{2} ) )

assume A9: <^p2,p3^> <> {} ; :: thesis: for b_{1}, b_{2} being M3(<^p2,p3^>) holds

( not b_{1} * n = b_{2} * n or b_{1} = b_{2} )

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: ( not f * n = g * n or f = g )

assume A11: f * n = g * n ; :: thesis: f = g

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: verum

for o1, o2 being Object of C

for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let D be non empty transitive SubCatStr of C; :: thesis: for o1, o2 being Object of C

for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let o1, o2 be Object of C; :: thesis: for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let p1, p2 be Object of D; :: thesis: for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let m be Morphism of o1,o2; :: thesis: for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds

( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

let n be Morphism of p1,p2; :: thesis: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} implies ( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) ) )

assume that

A1: p1 = o1 and

A2: p2 = o2 and

A3: ( m = n & <^p1,p2^> <> {} ) ; :: thesis: ( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

thus ( m is mono implies n is mono ) :: thesis: ( m is epi implies n is epi )

proof

assume A8:
m is epi
; :: thesis: n is epi
assume A4:
m is mono
; :: thesis: n is mono

let p3 be Object of D; :: according to ALTCAT_3:def 7 :: thesis: ( <^p3,p1^> = {} or for b_{1}, b_{2} being M3(<^p3,p1^>) holds

( not n * b_{1} = n * b_{2} or b_{1} = b_{2} ) )

assume A5: <^p3,p1^> <> {} ; :: thesis: for b_{1}, b_{2} being M3(<^p3,p1^>) holds

( not n * b_{1} = n * b_{2} or b_{1} = b_{2} )

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: ( not n * f = n * g or f = g )

assume A7: n * f = n * g ; :: thesis: f = g

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: verum

end;let p3 be Object of D; :: according to ALTCAT_3:def 7 :: thesis: ( <^p3,p1^> = {} or for b

( not n * b

assume A5: <^p3,p1^> <> {} ; :: thesis: for b

( not n * b

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: ( not n * f = n * g or f = g )

assume A7: n * f = n * g ; :: thesis: f = g

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: verum

let p3 be Object of D; :: according to ALTCAT_3:def 8 :: thesis: ( <^p2,p3^> = {} or for b

( not b

assume A9: <^p2,p3^> <> {} ; :: thesis: for b

( not b

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: ( not f * n = g * n or f = g )

assume A11: f * n = g * n ; :: thesis: f = g

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: verum