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 A1:
( p1 = o1 & p2 = o2 & 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 A2:
m is
mono
;
:: thesis: n is mono
let p3 be
object of
D;
:: according to ALTCAT_3:def 7 :: thesis: ( <^p3,p1^> = {} or for b1, b2 being M2(<^p3,p1^>) holds
( not n * b1 = n * b2 or b1 = b2 ) )
assume A3:
<^p3,p1^> <> {}
;
:: thesis: for b1, b2 being M2(<^p3,p1^>) holds
( not n * b1 = n * b2 or b1 = b2 )
let f,
g be
Morphism of
p3,
p1;
:: thesis: ( not n * f = n * g or f = g )
assume A4:
n * f = n * g
;
:: thesis: f = g
reconsider o3 =
p3 as
object of
C by ALTCAT_2:30;
A5:
<^o3,o1^> <> {}
by A1, A3, ALTCAT_2:32, XBOOLE_1:3;
reconsider f1 =
f,
g1 =
g as
Morphism of
o3,
o1 by A1, A3, ALTCAT_2:34;
m * f1 =
n * f
by A1, A3, ALTCAT_2:33
.=
m * g1
by A1, A3, A4, ALTCAT_2:33
;
hence
f = g
by A2, A5, ALTCAT_3:def 7;
:: thesis: verum
end;
assume A6:
m is epi
; :: thesis: n is epi
let p3 be object of D; :: according to ALTCAT_3:def 8 :: thesis: ( <^p2,p3^> = {} or for b1, b2 being M2(<^p2,p3^>) holds
( not b1 * n = b2 * n or b1 = b2 ) )
assume A7:
<^p2,p3^> <> {}
; :: thesis: for b1, b2 being M2(<^p2,p3^>) holds
( not b1 * n = b2 * n or b1 = b2 )
let f, g be Morphism of p2,p3; :: thesis: ( not f * n = g * n or f = g )
assume A8:
f * n = g * n
; :: thesis: f = g
reconsider o3 = p3 as object of C by ALTCAT_2:30;
A9:
<^o2,o3^> <> {}
by A1, A7, ALTCAT_2:32, XBOOLE_1:3;
reconsider f1 = f, g1 = g as Morphism of o2,o3 by A1, A7, ALTCAT_2:34;
f1 * m =
f * n
by A1, A7, ALTCAT_2:33
.=
g1 * m
by A1, A7, A8, ALTCAT_2:33
;
hence
f = g
by A6, A9, ALTCAT_3:def 8; :: thesis: verum