:: ALTCAT_3 semantic presentation

begin

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
let B be Morphism of o2,o1;
predA is_left_inverse_of B means :Def1: :: ALTCAT_3:def 1
A * B = idm o2;
end;

:: deftheorem Def1 defines is_left_inverse_of ALTCAT_3:def_1_:_
 for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o1 holds
( A is_left_inverse_of B iff A * B = idm o2 );

notation
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
let B be Morphism of o2,o1;
synonym B is_right_inverse_of A for A is_left_inverse_of B;
end;

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attrA is retraction  means :Def2: :: ALTCAT_3:def 2
 ex B being Morphism of o2,o1 st B is_right_inverse_of A;
end;

:: deftheorem Def2 defines retraction ALTCAT_3:def_2_:_
 for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is retraction iff ex B being Morphism of o2,o1 st B is_right_inverse_of A );

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attrA is coretraction  means :Def3: :: ALTCAT_3:def 3
 ex B being Morphism of o2,o1 st B is_left_inverse_of A;
end;

:: deftheorem Def3 defines coretraction ALTCAT_3:def_3_:_
 for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is coretraction iff ex B being Morphism of o2,o1 st B is_left_inverse_of A );

theorem Th1: :: ALTCAT_3:1
for C being non empty with_units AltCatStr
for o being object of C holds
( idm o is retraction & idm o is coretraction )
proof
let C be non empty with_units AltCatStr ; ::_thesis: for o being object of C holds
( idm o is retraction & idm o is coretraction )
let o be object of C; ::_thesis: ( idm o is retraction & idm o is coretraction )
 <^o,o^> <> {} by ALTCAT_1:19;
then  (idm o) * (idm o) = idm o by ALTCAT_1:def_17;
then  idm o is_left_inverse_of idm o by Def1;
hence  ( idm o is retraction & idm o is coretraction ) by Def2, Def3; ::_thesis: verum
end;

definition
let C be category;
let o1, o2 be object of C;
assume that
B1: <^o1,o2^> <> {} and
B2: <^o2,o1^> <> {} ;
let A be Morphism of o1,o2;
assume B3: ( A is retraction & A is coretraction ) ;
funcA "  ->  Morphism of o2,o1 means :Def4: :: ALTCAT_3:def 4
( it is_left_inverse_of A & it is_right_inverse_of A );
existence
 ex b1 being Morphism of o2,o1 st
( b1 is_left_inverse_of A & b1 is_right_inverse_of A )
proof
consider B1 being Morphism of o2,o1 such that
A1: B1 is_right_inverse_of A by B3, Def2;
take  B1 ; ::_thesis: ( B1 is_left_inverse_of A & B1 is_right_inverse_of A )
consider B2 being Morphism of o2,o1 such that
A2: B2 is_left_inverse_of A by B3, Def3;
B1 = (idm o1) * B1 by B2, ALTCAT_1:20
.= (B2 * A) * B1 by A2, Def1
.= B2 * (A * B1) by B1, B2, ALTCAT_1:21
.= B2 * (idm o2) by A1, Def1
.= B2 by B2, ALTCAT_1:def_17 ;
hence  ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Morphism of o2,o1 st b1 is_left_inverse_of A & b1 is_right_inverse_of A & b2 is_left_inverse_of A & b2 is_right_inverse_of A holds
b1 = b2
proof
let M1, M2 be Morphism of o2,o1; ::_thesis: ( M1 is_left_inverse_of A & M1 is_right_inverse_of A & M2 is_left_inverse_of A & M2 is_right_inverse_of A implies M1 = M2 )
assume that
A3: M1 is_left_inverse_of A and
 M1 is_right_inverse_of A and
 M2 is_left_inverse_of A and
A4: M2 is_right_inverse_of A ; ::_thesis: M1 = M2
thus M1 = M1 * (idm o2) by B2, ALTCAT_1:def_17
.= M1 * (A * M2) by A4, Def1
.= (M1 * A) * M2 by B1, B2, ALTCAT_1:21
.= (idm o1) * M2 by A3, Def1
.= M2 by B2, ALTCAT_1:20 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines " ALTCAT_3:def_4_:_
 for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
for b5 being Morphism of o2,o1 holds
( b5 = A " iff ( b5 is_left_inverse_of A & b5 is_right_inverse_of A ) );

theorem Th2: :: ALTCAT_3:2
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 )
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 )
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 )
let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is coretraction implies ( (A ") * A = idm o1 & A * (A ") = idm o2 ) )
assume  ( A is retraction & A is coretraction ) ; ::_thesis: ( (A ") * A = idm o1 & A * (A ") = idm o2 )
then  ( A " is_left_inverse_of A & A " is_right_inverse_of A ) by A1, Def4;
hence  ( (A ") * A = idm o1 & A * (A ") = idm o2 ) by Def1; ::_thesis: verum
end;

theorem Th3: :: ALTCAT_3:3
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A
let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is coretraction implies (A ") " = A )
assume A3: ( A is retraction & A is coretraction ) ; ::_thesis: (A ") " = A
then  A " is_left_inverse_of A by A1, A2, Def4;
then A4: A " is retraction by Def2;
A5: A " is_right_inverse_of A by A1, A2, A3, Def4;
then  A " is coretraction by Def3;
then A6: (A ") " is_right_inverse_of A " by A1, A2, A4, Def4;
thus (A ") " = (idm o2) * ((A ") ") by A1, ALTCAT_1:20
.= (A * (A ")) * ((A ") ") by A5, Def1
.= A * ((A ") * ((A ") ")) by A1, A2, ALTCAT_1:21
.= A * (idm o1) by A6, Def1
.= A by A1, ALTCAT_1:def_17 ; ::_thesis: verum
end;

theorem Th4: :: ALTCAT_3:4
for C being category
for o being object of C holds (idm o) " = idm o
proof
let C be category; ::_thesis: for o being object of C holds (idm o) " = idm o
let o be object of C; ::_thesis: (idm o) " = idm o
A1: <^o,o^> <> {} by ALTCAT_1:19;
 ( idm o is retraction & idm o is coretraction ) by Th1;
then A2: (idm o) " is_left_inverse_of idm o by A1, Def4;
thus (idm o) " = ((idm o) ") * (idm o) by A1, ALTCAT_1:def_17
.= idm o by A2, Def1 ; ::_thesis: verum
end;

definition
let C be category;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attrA is iso  means :Def5: :: ALTCAT_3:def 5
( A * (A ") = idm o2 & (A ") * A = idm o1 );
end;

:: deftheorem Def5 defines iso ALTCAT_3:def_5_:_
 for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is iso iff ( A * (A ") = idm o2 & (A ") * A = idm o1 ) );

theorem Th5: :: ALTCAT_3:5
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
proof
let C be category; ::_thesis: for o1, o2 being object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
let A be Morphism of o1,o2; ::_thesis: ( A is iso implies ( A is retraction & A is coretraction ) )
assume A1: A is iso ; ::_thesis: ( A is retraction & A is coretraction )
then  A * (A ") = idm o2 by Def5;
then  A " is_right_inverse_of A by Def1;
hence  A is retraction by Def2; ::_thesis: A is coretraction
 (A ") * A = idm o1 by A1, Def5;
then  A " is_left_inverse_of A by Def1;
hence  A is coretraction by Def3; ::_thesis: verum
end;

theorem Th6: :: ALTCAT_3:6
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
let A be Morphism of o1,o2; ::_thesis: ( A is iso iff ( A is retraction & A is coretraction ) )
thus  ( A is iso implies ( A is retraction & A is coretraction ) ) by Th5; ::_thesis: ( A is retraction & A is coretraction implies A is iso )
assume A2: ( A is retraction & A is coretraction ) ; ::_thesis: A is iso
then  A " is_right_inverse_of A by A1, Def4;
then A3: A * (A ") = idm o2 by Def1;
 A " is_left_inverse_of A by A1, A2, Def4;
then  (A ") * A = idm o1 by Def1;
hence  A is iso by A3, Def5; ::_thesis: verum
end;

theorem Th7: :: ALTCAT_3:7
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso implies ( B * A is iso & (B * A) " = (A ") * (B ") ) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {} ; ::_thesis: ( not A is iso or not B is iso or ( B * A is iso & (B * A) " = (A ") * (B ") ) )
assume that
A4: A is iso and
A5: B is iso ; ::_thesis: ( B * A is iso & (B * A) " = (A ") * (B ") )
consider A1 being Morphism of o2,o1 such that
A6: A1 = A " ;
A7: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2;
then A8: ( A is retraction & A is coretraction ) by A1, A4, Th6;
consider B1 being Morphism of o3,o2 such that
A9: B1 = B " ;
A10: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2;
then A11: ( B is retraction & B is coretraction ) by A2, A5, Th6;
A12: (B * A) * (A1 * B1) = B * (A * (A1 * B1)) by A1, A2, A3, ALTCAT_1:21
.= B * ((A * A1) * B1) by A1, A7, A10, ALTCAT_1:21
.= B * ((idm o2) * B1) by A1, A7, A8, A6, Th2
.= B * B1 by A10, ALTCAT_1:20
.= idm o3 by A2, A10, A11, A9, Th2 ;
then A13: A1 * B1 is_right_inverse_of B * A by Def1;
then A14: B * A is retraction by Def2;
A15: <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
then A16: (A1 * B1) * (B * A) = A1 * (B1 * (B * A)) by A7, A10, ALTCAT_1:21
.= A1 * ((B1 * B) * A) by A1, A2, A10, ALTCAT_1:21
.= A1 * ((idm o2) * A) by A2, A10, A11, A9, Th2
.= A1 * A by A1, ALTCAT_1:20
.= idm o1 by A1, A7, A8, A6, Th2 ;
then A17: A1 * B1 is_left_inverse_of B * A by Def1;
then  B * A is coretraction by Def3;
then  A1 * B1 = (B * A) " by A3, A15, A17, A13, A14, Def4;
hence  ( B * A is iso & (B * A) " = (A ") * (B ") ) by A6, A9, A16, A12, Def5; ::_thesis: verum
end;

definition
let C be category;
let o1, o2 be object of C;
predo1,o2 are_iso  means :Def6: :: ALTCAT_3:def 6
( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso );
reflexivity
 for o1 being object of C holds
( <^o1,o1^> <> {} & <^o1,o1^> <> {} & ex A being Morphism of o1,o1 st A is iso )
proof
let o be object of C; ::_thesis: ( <^o,o^> <> {} & <^o,o^> <> {} & ex A being Morphism of o,o st A is iso )
thus A1: ( <^o,o^> <> {} & <^o,o^> <> {} ) by ALTCAT_1:19; ::_thesis: ex A being Morphism of o,o st A is iso
take  idm o ; ::_thesis: idm o is iso
set A = idm o;
A2: ((idm o) ") * (idm o) = (idm o) * (idm o) by Th4
.= idm o by A1, ALTCAT_1:def_17 ;
(idm o) * ((idm o) ") = (idm o) * (idm o) by Th4
.= idm o by A1, ALTCAT_1:def_17 ;
hence  idm o is iso by A2, Def5; ::_thesis: verum
end;
symmetry
 for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso holds
( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso )
proof
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso implies ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso ) )
assume that
A3: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) and
A4: ex A being Morphism of o1,o2 st A is iso ; ::_thesis: ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso )
thus  ( <^o2,o1^> <> {} & <^o1,o2^> <> {} ) by A3; ::_thesis: ex A being Morphism of o2,o1 st A is iso
consider A being Morphism of o1,o2 such that
A5: A is iso by A4;
take A1 = A " ; ::_thesis: A1 is iso
A6: ( A is retraction & A is coretraction ) by A5, Th5;
then A7: (A1 ") * A1 = A * (A ") by A3, Th3
.= idm o2 by A3, A6, Th2 ;
A1 * (A1 ") = (A ") * A by A3, A6, Th3
.= idm o1 by A3, A6, Th2 ;
hence  A1 is iso by A7, Def5; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines are_iso ALTCAT_3:def_6_:_
 for C being category
for o1, o2 being object of C holds
( o1,o2 are_iso iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso ) );

theorem :: ALTCAT_3:8
for C being category
for o1, o2, o3 being object of C st o1,o2 are_iso & o2,o3 are_iso holds
o1,o3 are_iso
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C st o1,o2 are_iso & o2,o3 are_iso holds
o1,o3 are_iso
let o1, o2, o3 be object of C; ::_thesis: ( o1,o2 are_iso & o2,o3 are_iso implies o1,o3 are_iso )
assume that
A1: o1,o2 are_iso and
A2: o2,o3 are_iso ; ::_thesis: o1,o3 are_iso
A3: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) by A1, A2, Def6;
consider B being Morphism of o2,o3 such that
A4: B is iso by A2, Def6;
consider A being Morphism of o1,o2 such that
A5: A is iso by A1, Def6;
 ( <^o2,o1^> <> {} & <^o3,o2^> <> {} ) by A1, A2, Def6;
hence A6: ( <^o1,o3^> <> {} & <^o3,o1^> <> {} ) by A3, ALTCAT_1:def_2; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o3 st A is iso
take  B * A ; ::_thesis: B * A is iso
thus  B * A is iso by A3, A6, A5, A4, Th7; ::_thesis: verum
end;

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attrA is mono  means :Def7: :: ALTCAT_3:def 7
 for o being object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C;
end;

:: deftheorem Def7 defines mono ALTCAT_3:def_7_:_
 for C being non empty AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is mono iff for o being object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C );

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attrA is epi  means :Def8: :: ALTCAT_3:def 8
 for o being object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C;
end;

:: deftheorem Def8 defines epi ALTCAT_3:def_8_:_
 for C being non empty AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is epi iff for o being object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C );

theorem Th9: :: ALTCAT_3:9
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
proof
let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let B be Morphism of o2,o3; ::_thesis: ( A is mono & B is mono implies B * A is mono )
assume that
A3: A is mono and
A4: B is mono ; ::_thesis: B * A is mono
let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C )
assume A5: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C
then A6: <^o,o2^> <> {} by A1, ALTCAT_1:def_2;
let M1, M2 be Morphism of o,o1; ::_thesis: ( (B * A) * M1 = (B * A) * M2 implies M1 = M2 )
assume A7: (B * A) * M1 = (B * A) * M2 ; ::_thesis: M1 = M2
 ( (B * A) * M1 = B * (A * M1) & (B * A) * M2 = B * (A * M2) ) by A1, A2, A5, ALTCAT_1:21;
then  A * M1 = A * M2 by A4, A7, A6, Def7;
hence  M1 = M2 by A3, A5, Def7; ::_thesis: verum
end;

theorem Th10: :: ALTCAT_3:10
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi
proof
let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi
let B be Morphism of o2,o3; ::_thesis: ( A is epi & B is epi implies B * A is epi )
assume that
A3: A is epi and
A4: B is epi ; ::_thesis: B * A is epi
let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o3,o^> <> {} implies for B, C being Morphism of o3,o st B * (B * A) = C * (B * A) holds
B = C )
assume A5: <^o3,o^> <> {} ; ::_thesis: for B, C being Morphism of o3,o st B * (B * A) = C * (B * A) holds
B = C
then A6: <^o2,o^> <> {} by A2, ALTCAT_1:def_2;
let M1, M2 be Morphism of o3,o; ::_thesis: ( M1 * (B * A) = M2 * (B * A) implies M1 = M2 )
assume A7: M1 * (B * A) = M2 * (B * A) ; ::_thesis: M1 = M2
 ( M1 * (B * A) = (M1 * B) * A & M2 * (B * A) = (M2 * B) * A ) by A1, A2, A5, ALTCAT_1:21;
then  M1 * B = M2 * B by A3, A7, A6, Def8;
hence  M1 = M2 by A4, A5, Def8; ::_thesis: verum
end;

theorem :: ALTCAT_3:11
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono
proof
let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st B * A is mono holds
A is mono
let B be Morphism of o2,o3; ::_thesis: ( B * A is mono implies A is mono )
assume A2: B * A is mono ; ::_thesis: A is mono
let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A3: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let M1, M2 be Morphism of o,o1; ::_thesis: ( A * M1 = A * M2 implies M1 = M2 )
assume A4: A * M1 = A * M2 ; ::_thesis: M1 = M2
 ( (B * A) * M1 = B * (A * M1) & (B * A) * M2 = B * (A * M2) ) by A1, A3, ALTCAT_1:21;
hence  M1 = M2 by A2, A3, A4, Def7; ::_thesis: verum
end;

theorem :: ALTCAT_3:12
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi
proof
let C be non empty transitive associative AltCatStr ; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st B * A is epi holds
B is epi
let B be Morphism of o2,o3; ::_thesis: ( B * A is epi implies B is epi )
assume A2: B * A is epi ; ::_thesis: B is epi
let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o3,o^> <> {} implies for B, C being Morphism of o3,o st B * B = C * B holds
B = C )
assume A3: <^o3,o^> <> {} ; ::_thesis: for B, C being Morphism of o3,o st B * B = C * B holds
B = C
let M1, M2 be Morphism of o3,o; ::_thesis: ( M1 * B = M2 * B implies M1 = M2 )
assume A4: M1 * B = M2 * B ; ::_thesis: M1 = M2
 ( (M1 * B) * A = M1 * (B * A) & (M2 * B) * A = M2 * (B * A) ) by A1, A3, ALTCAT_1:21;
hence  M1 = M2 by A2, A3, A4, Def8; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_C_being_non_empty_with_units_AltCatStr_
for_a_being_object_of_C_holds_
(_idm_a_is_epi_&_idm_a_is_mono_)
let C be non empty with_units AltCatStr ; ::_thesis: for a being object of C holds
( idm a is epi & idm a is mono )
let a be object of C; ::_thesis: ( idm a is epi & idm a is mono )
thus  idm a is epi ::_thesis: idm a is mono
proof
let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^a,o^> <> {} implies for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C )
assume A1: <^a,o^> <> {} ; ::_thesis: for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C
let B, C be Morphism of a,o; ::_thesis: ( B * (idm a) = C * (idm a) implies B = C )
assume A2: B * (idm a) = C * (idm a) ; ::_thesis: B = C
thus B = B * (idm a) by A1, ALTCAT_1:def_17
.= C by A1, A2, ALTCAT_1:def_17 ; ::_thesis: verum
end;
thus  idm a is mono ::_thesis: verum
proof
let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,a^> <> {} implies for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C )
assume A3: <^o,a^> <> {} ; ::_thesis: for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C
let B, C be Morphism of o,a; ::_thesis: ( (idm a) * B = (idm a) * C implies B = C )
assume A4: (idm a) * B = (idm a) * C ; ::_thesis: B = C
thus B = (idm a) * B by A3, ALTCAT_1:20
.= C by A3, A4, ALTCAT_1:20 ; ::_thesis: verum
end;
end;

theorem :: ALTCAT_3:13
for X being non empty set
for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
proof
let X be non empty set ; ::_thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let o1, o2 be object of (EnsCat X); ::_thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one ) )
assume A1: <^o1,o2^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let A be Morphism of o1,o2; ::_thesis: for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let F be Function of o1,o2; ::_thesis: ( F = A implies ( A is mono iff F is one-to-one ) )
assume A2: F = A ; ::_thesis: ( A is mono iff F is one-to-one )
percases ( o2 <> {} or o2 = {} ) ;
suppose o2 <> {} ; ::_thesis: ( A is mono iff F is one-to-one )
then A3: dom F = o1 by FUNCT_2:def_1;
thus  ( A is mono implies F is one-to-one ) ::_thesis: ( F is one-to-one implies A is mono )
proof
set o = o1;
assume A4: A is mono ; ::_thesis: F is one-to-one
assume  not F is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set  such that
A5: x1 in dom F and
A6: x2 in dom F and
A7: F . x1 = F . x2 and
A8: x1 <> x2 by FUNCT_1:def_4;
set C = o1 --> x2;
set B = o1 --> x1;
A9: dom (o1 --> x2) = o1 by FUNCOP_1:13;
A10: rng (o1 --> x2) c= o1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o1 --> x2) or y in o1 )
assume  y in rng (o1 --> x2) ; ::_thesis: y in o1
then  ex x being set st
( x in dom (o1 --> x2) & (o1 --> x2) . x = y ) by FUNCT_1:def_3;
hence  y in o1 by A3, A6, A9, FUNCOP_1:7; ::_thesis: verum
end;
then A11: dom (F * (o1 --> x2)) = o1 by A3, A9, RELAT_1:27;
 o1 --> x2 in Funcs (o1,o1) by A9, A10, FUNCT_2:def_2;
then reconsider C1 = o1 --> x2 as Morphism of o1,o1 by ALTCAT_1:def_14;
set o9 = the Element of o1;
A12: <^o1,o1^> <> {} by ALTCAT_1:19;
 (o1 --> x1) . the Element of o1 = x1 by A3, A5, FUNCOP_1:7;
then A13: (o1 --> x1) . the Element of o1 <> (o1 --> x2) . the Element of o1 by A3, A5, A8, FUNCOP_1:7;
A14: dom (o1 --> x1) = o1 by FUNCOP_1:13;
A15: rng (o1 --> x1) c= o1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o1 --> x1) or y in o1 )
assume  y in rng (o1 --> x1) ; ::_thesis: y in o1
then  ex x being set st
( x in dom (o1 --> x1) & (o1 --> x1) . x = y ) by FUNCT_1:def_3;
hence  y in o1 by A3, A5, A14, FUNCOP_1:7; ::_thesis: verum
end;
then  o1 --> x1 in Funcs (o1,o1) by A14, FUNCT_2:def_2;
then reconsider B1 = o1 --> x1 as Morphism of o1,o1 by ALTCAT_1:def_14;
A16: dom (F * (o1 --> x1)) = o1 by A3, A14, A15, RELAT_1:27;
now__::_thesis:_for_z_being_set_st_z_in_o1_holds_
(F_*_(o1_-->_x1))_._z_=_(F_*_(o1_-->_x2))_._z
let z be set ; ::_thesis: ( z in o1 implies (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z )
assume A17: z in o1 ; ::_thesis: (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z
hence (F * (o1 --> x1)) . z = F . ((o1 --> x1) . z) by A16, FUNCT_1:12
.= F . x2 by A7, A17, FUNCOP_1:7
.= F . ((o1 --> x2) . z) by A17, FUNCOP_1:7
.= (F * (o1 --> x2)) . z by A11, A17, FUNCT_1:12 ;
::_thesis: verum
end;
then  F * (o1 --> x1) = F * (o1 --> x2) by A16, A11, FUNCT_1:2;
then A * B1 = F * (o1 --> x2) by A1, A2, A12, ALTCAT_1:16
.= A * C1 by A1, A2, A12, ALTCAT_1:16 ;
hence  contradiction by A4, A12, A13, Def7; ::_thesis: verum
end;
thus  ( F is one-to-one implies A is mono ) ::_thesis: verum
proof
assume A18: F is one-to-one ; ::_thesis: A is mono
let o be object of (EnsCat X); :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A19: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
then A20: <^o,o2^> <> {} by A1, ALTCAT_1:def_2;
let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C )
A21: <^o,o1^> = Funcs (o,o1) by ALTCAT_1:def_14;
then consider B1 being Function such that
A22: B1 = B and
A23: dom B1 = o and
A24: rng B1 c= o1 by A19, FUNCT_2:def_2;
consider C1 being Function such that
A25: C1 = C and
A26: dom C1 = o and
A27: rng C1 c= o1 by A19, A21, FUNCT_2:def_2;
assume  A * B = A * C ; ::_thesis: B = C
then A28: F * B1 = A * C by A1, A2, A19, A22, A20, ALTCAT_1:16
.= F * C1 by A1, A2, A19, A25, A20, ALTCAT_1:16 ;
now__::_thesis:_for_z_being_set_st_z_in_o_holds_
B1_._z_=_C1_._z
let z be set ; ::_thesis: ( z in o implies B1 . z = C1 . z )
assume A29: z in o ; ::_thesis: B1 . z = C1 . z
then  F . (B1 . z) = (F * B1) . z by A23, FUNCT_1:13;
then A30: F . (B1 . z) = F . (C1 . z) by A26, A28, A29, FUNCT_1:13;
 ( B1 . z in rng B1 & C1 . z in rng C1 ) by A23, A26, A29, FUNCT_1:def_3;
hence  B1 . z = C1 . z by A3, A18, A24, A27, A30, FUNCT_1:def_4; ::_thesis: verum
end;
hence  B = C by A22, A23, A25, A26, FUNCT_1:2; ::_thesis: verum
end;
end;
supposeA31: o2 = {} ; ::_thesis: ( A is mono iff F is one-to-one )
then  F = {} ;
hence  ( A is mono implies F is one-to-one ) ; ::_thesis: ( F is one-to-one implies A is mono )
thus  ( F is one-to-one implies A is mono ) ::_thesis: verum
proof
set x = the Element of Funcs (o1,o2);
assume  F is one-to-one ; ::_thesis: A is mono
let o be object of (EnsCat X); :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A32: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
 <^o1,o2^> = Funcs (o1,o2) by ALTCAT_1:def_14;
then consider f being Function such that
 f = the Element of Funcs (o1,o2) and
A33: dom f = o1 and
A34: rng f c= o2 by A1, FUNCT_2:def_2;
let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C )
A35: <^o,o1^> = Funcs (o,o1) by ALTCAT_1:def_14;
then consider B1 being Function such that
A36: B1 = B and
A37: dom B1 = o and
A38: rng B1 c= o1 by A32, FUNCT_2:def_2;
 rng f = {} by A31, A34, XBOOLE_1:3;
then  dom f = {} by RELAT_1:42;
then A39: rng B1 = {} by A38, A33, XBOOLE_1:3;
then A40: dom B1 = {} by RELAT_1:42;
assume  A * B = A * C ; ::_thesis: B = C
consider C1 being Function such that
A41: C1 = C and
A42: dom C1 = o and
 rng C1 c= o1 by A32, A35, FUNCT_2:def_2;
B1 = {} by A39, RELAT_1:41
.= C1 by A37, A42, A40, RELAT_1:41 ;
hence  B = C by A36, A41; ::_thesis: verum
end;
end;
end;
end;

theorem :: ALTCAT_3:14
for X being non empty with_non-empty_elements set
for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
proof
let X be non empty with_non-empty_elements set ; ::_thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let o1, o2 be object of (EnsCat X); ::_thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto ) )
assume A1: <^o1,o2^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let A be Morphism of o1,o2; ::_thesis: for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let F be Function of o1,o2; ::_thesis: ( F = A implies ( A is epi iff F is onto ) )
assume A2: F = A ; ::_thesis: ( A is epi iff F is onto )
percases ( for x being set st x in X holds
x is trivial or ex x being set st
( x in X & not x is trivial ) ) ;
supposeA3: for x being set st x in X holds
x is trivial ; ::_thesis: ( A is epi iff F is onto )
thus  ( A is epi implies F is onto ) ::_thesis: ( F is onto implies A is epi )
proof
assume  A is epi ; ::_thesis: F is onto
now__::_thesis:_F_is_onto
percases ( o2 = {} or o2 <> {} ) ;
supposeA4: o2 = {} ; ::_thesis: F is onto
then  F = {} ;
hence  F is onto by A4, FUNCT_2:def_3, RELAT_1:38; ::_thesis: verum
end;
supposeA5: o2 <> {} ; ::_thesis: F is onto
A6: o1 is Element of X by ALTCAT_1:def_14;
then  o1 is trivial by A3;
then consider z being set  such that
A7: o1 = {z} by A6, ZFMISC_1:131;
 dom F = {z} by A5, A7, FUNCT_2:def_1;
then A8: rng F <> {} by RELAT_1:42;
 o2 is Element of X by ALTCAT_1:def_14;
then  o2 is trivial by A3;
then consider y being set  such that
A9: o2 = {y} by A5, ZFMISC_1:131;
 rng F c= {y} by A9, RELAT_1:def_19;
then  rng F = {y} by A8, ZFMISC_1:33;
hence  F is onto by A9, FUNCT_2:def_3; ::_thesis: verum
end;
end;
end;
hence  F is onto ; ::_thesis: verum
end;
thus  ( F is onto implies A is epi ) ::_thesis: verum
proof
assume A10: F is onto ; ::_thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A11: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
then A12: <^o1,o^> <> {} by A1, ALTCAT_1:def_2;
let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C )
A13: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14;
then consider B1 being Function such that
A14: B1 = B and
A15: dom B1 = o2 and
 rng B1 c= o by A11, FUNCT_2:def_2;
consider C1 being Function such that
A16: C1 = C and
A17: dom C1 = o2 and
 rng C1 c= o by A11, A13, FUNCT_2:def_2;
assume  B * A = C * A ; ::_thesis: B = C
then A18: B1 * F = C * A by A1, A2, A11, A14, A12, ALTCAT_1:16
.= C1 * F by A1, A2, A11, A16, A12, ALTCAT_1:16 ;
now__::_thesis:_not_B1_<>_C1
assume  B1 <> C1 ; ::_thesis: contradiction
then consider z being set  such that
A19: z in o2 and
A20: B1 . z <> C1 . z by A15, A17, FUNCT_1:2;
 z in rng F by A10, A19, FUNCT_2:def_3;
then consider x being set  such that
A21: x in dom F and
A22: F . x = z by FUNCT_1:def_3;
 B1 . (F . x) = (B1 * F) . x by A21, FUNCT_1:13;
hence  contradiction by A18, A20, A21, A22, FUNCT_1:13; ::_thesis: verum
end;
hence  B = C by A14, A16; ::_thesis: verum
end;
end;
supposeA23: ex x being set st
( x in X & not x is trivial ) ; ::_thesis: ( A is epi iff F is onto )
now__::_thesis:_(_(_A_is_epi_implies_F_is_onto_)_&_(_F_is_onto_implies_A_is_epi_)_)
percases ( o2 <> {} or o2 = {} ) ;
supposeA24: o2 <> {} ; ::_thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )
consider o being set  such that
A25: o in X and
A26: not o is trivial by A23;
reconsider o = o as object of (EnsCat X) by A25, ALTCAT_1:def_14;
A27: dom F = o1 by A24, FUNCT_2:def_1;
thus  ( A is epi implies F is onto ) ::_thesis: ( F is onto implies A is epi )
proof
set k = the Element of o;
A28: rng F c= o2 by RELAT_1:def_19;
reconsider ok = o \ { the Element of o} as non empty set by A26, REALSET1:3;
assume that
A29: A is epi and
A30: not F is onto ; ::_thesis: contradiction
 rng F <> o2 by A30, FUNCT_2:def_3;
then  not o2 c= rng F by A28, XBOOLE_0:def_10;
then consider y being set  such that
A31: y in o2 and
A32: not y in rng F by TARSKI:def_3;
set C = o2 --> the Element of o;
A33: dom (o2 --> the Element of o) = o2 by FUNCOP_1:13;
A34: o <> {} by A25;
then A35: the Element of o in o ;
 rng (o2 --> the Element of o) c= o
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (o2 --> the Element of o) or y in o )
assume  y in rng (o2 --> the Element of o) ; ::_thesis: y in o
then  ex x being set st
( x in dom (o2 --> the Element of o) & (o2 --> the Element of o) . x = y ) by FUNCT_1:def_3;
hence  y in o by A35, A33, FUNCOP_1:7; ::_thesis: verum
end;
then  o2 --> the Element of o in Funcs (o2,o) by A33, FUNCT_2:def_2;
then reconsider C1 = o2 --> the Element of o as Morphism of o2,o by ALTCAT_1:def_14;
set l = the Element of ok;
A36: not the Element of ok in { the Element of o} by XBOOLE_0:def_5;
reconsider l = the Element of ok as Element of o by XBOOLE_0:def_5;
A37: the Element of o <> l by A36, TARSKI:def_1;
deffunc H1( set ) ->  Element of o = IFEQ ($1,y,l, the Element of o);
consider B being Function such that
A38: dom B = o2 and
A39: for x being set st x in o2 holds
B . x = H1(x) from FUNCT_1:sch_3();
A40: dom (B * F) = o1 by A27, A28, A38, RELAT_1:27;
A41: rng B c= o
proof
let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in rng B or y1 in o )
assume  y1 in rng B ; ::_thesis: y1 in o
then consider x being set  such that
A42: ( x in dom B & B . x = y1 ) by FUNCT_1:def_3;
percases ( x = y or x <> y ) ;
supposeA43: x = y ; ::_thesis: y1 in o
y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42
.= l by A43, FUNCOP_1:def_8 ;
hence  y1 in o by A34; ::_thesis: verum
end;
supposeA44: x <> y ; ::_thesis: y1 in o
y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42
.= the Element of o by A44, FUNCOP_1:def_8 ;
hence  y1 in o by A34; ::_thesis: verum
end;
end;
end;
then A45: B in Funcs (o2,o) by A38, FUNCT_2:def_2;
then A46: B in <^o2,o^> by ALTCAT_1:def_14;
reconsider B1 = B as Morphism of o2,o by A45, ALTCAT_1:def_14;
 for z being set st z in rng (B * F) holds
z in rng B by FUNCT_1:14;
then  rng (B * F) c= rng B by TARSKI:def_3;
then  rng (B * F) c= o by A41, XBOOLE_1:1;
then  B * F in Funcs (o1,o) by A40, FUNCT_2:def_2;
then A47: B * F in <^o1,o^> by ALTCAT_1:def_14;
B . y = IFEQ (y,y,l, the Element of o) by A31, A39
.= l by FUNCOP_1:def_8 ;
then A48: not B = o2 --> the Element of o by A31, A37, FUNCOP_1:7;
A49: dom ((o2 --> the Element of o) * F) = o1 by A27, A28, A33, RELAT_1:27;
now__::_thesis:_for_z_being_set_st_z_in_o1_holds_
(B_*_F)_._z_=_((o2_-->_the_Element_of_o)_*_F)_._z
let z be set ; ::_thesis: ( z in o1 implies (B * F) . z = ((o2 --> the Element of o) * F) . z )
assume A50: z in o1 ; ::_thesis: (B * F) . z = ((o2 --> the Element of o) * F) . z
then A51: F . z in rng F by A27, FUNCT_1:def_3;
then A52: B . (F . z) = IFEQ ((F . z),y,l, the Element of o) by A28, A39
.= the Element of o by A32, A51, FUNCOP_1:def_8 ;
thus (B * F) . z = B . (F . z) by A40, A50, FUNCT_1:12
.= (o2 --> the Element of o) . (F . z) by A28, A51, A52, FUNCOP_1:7
.= ((o2 --> the Element of o) * F) . z by A49, A50, FUNCT_1:12 ; ::_thesis: verum
end;
then  B * F = (o2 --> the Element of o) * F by A40, A49, FUNCT_1:2;
then B1 * A = (o2 --> the Element of o) * F by A1, A2, A46, A47, ALTCAT_1:16
.= C1 * A by A1, A2, A46, A47, ALTCAT_1:16 ;
hence  contradiction by A29, A48, A46, Def8; ::_thesis: verum
end;
thus  ( F is onto implies A is epi ) ::_thesis: verum
proof
assume A53: F is onto ; ::_thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A54: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
then A55: <^o1,o^> <> {} by A1, ALTCAT_1:def_2;
let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C )
A56: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14;
then consider B1 being Function such that
A57: B1 = B and
A58: dom B1 = o2 and
 rng B1 c= o by A54, FUNCT_2:def_2;
consider C1 being Function such that
A59: C1 = C and
A60: dom C1 = o2 and
 rng C1 c= o by A54, A56, FUNCT_2:def_2;
assume  B * A = C * A ; ::_thesis: B = C
then A61: B1 * F = C * A by A1, A2, A54, A57, A55, ALTCAT_1:16
.= C1 * F by A1, A2, A54, A59, A55, ALTCAT_1:16 ;
now__::_thesis:_not_B1_<>_C1
assume  B1 <> C1 ; ::_thesis: contradiction
then consider z being set  such that
A62: z in o2 and
A63: B1 . z <> C1 . z by A58, A60, FUNCT_1:2;
 z in rng F by A53, A62, FUNCT_2:def_3;
then consider x being set  such that
A64: x in dom F and
A65: F . x = z by FUNCT_1:def_3;
 B1 . (F . x) = (B1 * F) . x by A64, FUNCT_1:13;
hence  contradiction by A61, A63, A64, A65, FUNCT_1:13; ::_thesis: verum
end;
hence  B = C by A57, A59; ::_thesis: verum
end;
end;
supposeA66: o2 = {} ; ::_thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )
then  F = {} ;
hence  ( A is epi implies F is onto ) by A66, FUNCT_2:def_3, RELAT_1:38; ::_thesis: ( F is onto implies A is epi )
thus  ( F is onto implies A is epi ) ::_thesis: verum
proof
assume  F is onto ; ::_thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A67: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C )
A68: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def_14;
then consider B1 being Function such that
A69: B1 = B and
A70: dom B1 = o2 and
 rng B1 c= o by A67, FUNCT_2:def_2;
A71: ex C1 being Function st
( C1 = C & dom C1 = o2 & rng C1 c= o ) by A67, A68, FUNCT_2:def_2;
assume  B * A = C * A ; ::_thesis: B = C
 B1 = {} by A66, A70, RELAT_1:41;
hence  B = C by A66, A69, A71, RELAT_1:41; ::_thesis: verum
end;
end;
end;
end;
hence  ( A is epi iff F is onto ) ; ::_thesis: verum
end;
end;
end;

theorem Th15: :: ALTCAT_3:15
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction holds
A is epi
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction holds
A is epi
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction holds
A is epi )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is retraction holds
A is epi
let A be Morphism of o1,o2; ::_thesis: ( A is retraction implies A is epi )
assume  A is retraction ; ::_thesis: A is epi
then consider R being Morphism of o2,o1 such that
A2: R is_right_inverse_of A by Def2;
let o be object of C; :: according to ALTCAT_3:def_8 ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A3: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C )
assume A4: B * A = C * A ; ::_thesis: B = C
thus B = B * (idm o2) by A3, ALTCAT_1:def_17
.= B * (A * R) by A2, Def1
.= (C * A) * R by A1, A3, A4, ALTCAT_1:21
.= C * (A * R) by A1, A3, ALTCAT_1:21
.= C * (idm o2) by A2, Def1
.= C by A3, ALTCAT_1:def_17 ; ::_thesis: verum
end;

theorem Th16: :: ALTCAT_3:16
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is coretraction holds
A is mono
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is coretraction holds
A is mono
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is coretraction holds
A is mono )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is coretraction holds
A is mono
let A be Morphism of o1,o2; ::_thesis: ( A is coretraction implies A is mono )
assume  A is coretraction ; ::_thesis: A is mono
then consider R being Morphism of o2,o1 such that
A2: R is_left_inverse_of A by Def3;
let o be object of C; :: according to ALTCAT_3:def_7 ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A3: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C )
assume A4: A * B = A * C ; ::_thesis: B = C
thus B = (idm o1) * B by A3, ALTCAT_1:20
.= (R * A) * B by A2, Def1
.= R * (A * C) by A1, A3, A4, ALTCAT_1:21
.= (R * A) * C by A1, A3, ALTCAT_1:21
.= (idm o1) * C by A2, Def1
.= C by A3, ALTCAT_1:20 ; ::_thesis: verum
end;

theorem :: ALTCAT_3:17
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
proof
let C be category; ::_thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let o1, o2 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; ::_thesis: for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let A be Morphism of o1,o2; ::_thesis: ( A is iso implies ( A is mono & A is epi ) )
assume  A is iso ; ::_thesis: ( A is mono & A is epi )
then A2: ( A is retraction & A is coretraction ) by A1, Th6;
A3: for o being object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C
proof
let o be object of C; ::_thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A4: <^o2,o^> <> {} ; ::_thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; ::_thesis: ( B * A = C * A implies B = C )
assume  B * A = C * A ; ::_thesis: B = C
then  B * (A * (A ")) = (C * A) * (A ") by A1, A4, ALTCAT_1:21;
then  B * (idm o2) = (C * A) * (A ") by A1, A2, Th2;
then  B * (idm o2) = C * (A * (A ")) by A1, A4, ALTCAT_1:21;
then  B * (idm o2) = C * (idm o2) by A1, A2, Th2;
then  B = C * (idm o2) by A4, ALTCAT_1:def_17;
hence  B = C by A4, ALTCAT_1:def_17; ::_thesis: verum
end;
 for o being object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
proof
let o be object of C; ::_thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A5: <^o,o1^> <> {} ; ::_thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; ::_thesis: ( A * B = A * C implies B = C )
assume  A * B = A * C ; ::_thesis: B = C
then  ((A ") * A) * B = (A ") * (A * C) by A1, A5, ALTCAT_1:21;
then  (idm o1) * B = (A ") * (A * C) by A1, A2, Th2;
then  (idm o1) * B = ((A ") * A) * C by A1, A5, ALTCAT_1:21;
then  (idm o1) * B = (idm o1) * C by A1, A2, Th2;
then  B = (idm o1) * C by A5, ALTCAT_1:20;
hence  B = C by A5, ALTCAT_1:20; ::_thesis: verum
end;
hence  ( A is mono & A is epi ) by A3, Def7, Def8; ::_thesis: verum
end;

theorem Th18: :: ALTCAT_3:18
for C being category
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
A4: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2;
A5: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2;
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
let B be Morphism of o2,o3; ::_thesis: ( A is retraction & B is retraction implies B * A is retraction )
assume that
A6: A is retraction and
A7: B is retraction ; ::_thesis: B * A is retraction
consider A1 being Morphism of o2,o1 such that
A8: A1 is_right_inverse_of A by A6, Def2;
consider B1 being Morphism of o3,o2 such that
A9: B1 is_right_inverse_of B by A7, Def2;
consider G being Morphism of o3,o1 such that
A10: G = A1 * B1 ;
take  G ; :: according to ALTCAT_3:def_2 ::_thesis: G is_right_inverse_of B * A
(B * A) * G = B * (A * (A1 * B1)) by A1, A2, A3, A10, ALTCAT_1:21
.= B * ((A * A1) * B1) by A1, A4, A5, ALTCAT_1:21
.= B * ((idm o2) * B1) by A8, Def1
.= B * B1 by A5, ALTCAT_1:20
.= idm o3 by A9, Def1 ;
hence  G is_right_inverse_of B * A by Def1; ::_thesis: verum
end;

theorem Th19: :: ALTCAT_3:19
for C being category
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
let o1, o2, o3 be object of C; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {} ; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
A4: <^o2,o1^> <> {} by A2, A3, ALTCAT_1:def_2;
A5: <^o3,o2^> <> {} by A1, A3, ALTCAT_1:def_2;
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
let B be Morphism of o2,o3; ::_thesis: ( A is coretraction & B is coretraction implies B * A is coretraction )
assume that
A6: A is coretraction and
A7: B is coretraction ; ::_thesis: B * A is coretraction
consider A1 being Morphism of o2,o1 such that
A8: A1 is_left_inverse_of A by A6, Def3;
consider B1 being Morphism of o3,o2 such that
A9: B1 is_left_inverse_of B by A7, Def3;
consider G being Morphism of o3,o1 such that
A10: G = A1 * B1 ;
take  G ; :: according to ALTCAT_3:def_3 ::_thesis: G is_left_inverse_of B * A
A11: <^o2,o2^> <> {} by ALTCAT_1:19;
G * (B * A) = ((A1 * B1) * B) * A by A1, A2, A3, A10, ALTCAT_1:21
.= (A1 * (B1 * B)) * A by A2, A4, A5, ALTCAT_1:21
.= (A1 * (idm o2)) * A by A9, Def1
.= A1 * ((idm o2) * A) by A1, A4, A11, ALTCAT_1:21
.= A1 * A by A1, ALTCAT_1:20
.= idm o1 by A8, Def1 ;
hence  G is_left_inverse_of B * A by Def1; ::_thesis: verum
end;

theorem Th20: :: ALTCAT_3:20
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
proof
let C be category; ::_thesis: for o1, o2 being object of C
for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let A be Morphism of o1,o2; ::_thesis: ( A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso )
assume that
A1: A is retraction and
A2: A is mono and
A3: <^o1,o2^> <> {} and
A4: <^o2,o1^> <> {} ; ::_thesis: A is iso
consider B being Morphism of o2,o1 such that
A5: B is_right_inverse_of A by A1, Def2;
 (A * B) * A = (idm o2) * A by A5, Def1;
then  A * (B * A) = (idm o2) * A by A3, A4, ALTCAT_1:21;
then  A * (B * A) = A by A3, ALTCAT_1:20;
then A6: ( <^o1,o1^> <> {} & A * (B * A) = A * (idm o1) ) by A3, ALTCAT_1:19, ALTCAT_1:def_17;
then  B * A = idm o1 by A2, Def7;
then A7: B is_left_inverse_of A by Def1;
then A8: A is coretraction by Def3;
then A9: A * (A ") = A * B by A1, A3, A4, A5, A7, Def4
.= idm o2 by A5, Def1 ;
(A ") * A = B * A by A1, A3, A4, A5, A7, A8, Def4
.= idm o1 by A2, A6, Def7 ;
hence  A is iso by A9, Def5; ::_thesis: verum
end;

theorem :: ALTCAT_3:21
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
proof
let C be category; ::_thesis: for o1, o2 being object of C
for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let o1, o2 be object of C; ::_thesis: for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let A be Morphism of o1,o2; ::_thesis: ( A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso )
assume that
A1: A is coretraction and
A2: A is epi and
A3: <^o1,o2^> <> {} and
A4: <^o2,o1^> <> {} ; ::_thesis: A is iso
consider B being Morphism of o2,o1 such that
A5: B is_left_inverse_of A by A1, Def3;
 A * (B * A) = A * (idm o1) by A5, Def1;
then  A * (B * A) = A by A3, ALTCAT_1:def_17;
then  A * (B * A) = (idm o2) * A by A3, ALTCAT_1:20;
then A6: ( <^o2,o2^> <> {} & (A * B) * A = (idm o2) * A ) by A3, A4, ALTCAT_1:19, ALTCAT_1:21;
then  A * B = idm o2 by A2, Def8;
then A7: B is_right_inverse_of A by Def1;
then A8: A is retraction by Def2;
then A9: (A ") * A = B * A by A1, A3, A4, A5, A7, Def4
.= idm o1 by A5, Def1 ;
A * (A ") = A * B by A1, A3, A4, A5, A7, A8, Def4
.= idm o2 by A2, A6, Def8 ;
hence  A is iso by A9, Def5; ::_thesis: verum
end;

theorem :: ALTCAT_3:22
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction implies B is retraction )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; ::_thesis: ( not B * A is retraction or B is retraction )
assume  B * A is retraction ; ::_thesis: B is retraction
then consider G being Morphism of o3,o1 such that
A2: G is_right_inverse_of B * A by Def2;
 (B * A) * G = idm o3 by A2, Def1;
then  B * (A * G) = idm o3 by A1, ALTCAT_1:21;
then  A * G is_right_inverse_of B by Def1;
hence  B is retraction by Def2; ::_thesis: verum
end;

theorem :: ALTCAT_3:23
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let o1, o2, o3 be object of C; ::_thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let A be Morphism of o1,o2; ::_thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let B be Morphism of o2,o3; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction implies A is coretraction )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; ::_thesis: ( not B * A is coretraction or A is coretraction )
assume  B * A is coretraction ; ::_thesis: A is coretraction
then consider G being Morphism of o3,o1 such that
A2: G is_left_inverse_of B * A by Def3;
A3: (G * B) * A = G * (B * A) by A1, ALTCAT_1:21;
 G * (B * A) = idm o1 by A2, Def1;
then  G * B is_left_inverse_of A by A3, Def1;
hence  A is coretraction by Def3; ::_thesis: verum
end;

theorem :: ALTCAT_3:24
for C being category st ( for o1, o2 being object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ) holds
for a, b being object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
proof
let C be category; ::_thesis: ( ( for o1, o2 being object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ) implies for a, b being object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso )
assume A1: for o1, o2 being object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ; ::_thesis: for a, b being object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
thus  for a, b being object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso ::_thesis: verum
proof
let a, b be object of C; ::_thesis: for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
let A be Morphism of a,b; ::_thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies A is iso )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; ::_thesis: A is iso
A4: A is retraction by A1;
 A is coretraction
proof
consider A1 being Morphism of b,a such that
A5: A1 is_right_inverse_of A by A4, Def2;
 A1 * (A * A1) = A1 * (idm b) by A5, Def1;
then  A1 * (A * A1) = A1 by A3, ALTCAT_1:def_17;
then  (A1 * A) * A1 = A1 by A2, A3, ALTCAT_1:21;
then A6: (A1 * A) * A1 = (idm a) * A1 by A3, ALTCAT_1:20;
 ( A1 is epi & <^a,a^> <> {} ) by A1, A2, A3, Th15, ALTCAT_1:19;
then  A1 * A = idm a by A6, Def8;
then  A1 is_left_inverse_of A by Def1;
hence  A is coretraction by Def3; ::_thesis: verum
end;
hence  A is iso by A2, A3, A4, Th6; ::_thesis: verum
end;
end;

registration
let C be non empty with_units AltCatStr ;
let o be object of C;
cluster retraction coretraction mono epi for Element of <^o,o^>;
existence
 ex b1 being Morphism of o,o st
( b1 is mono & b1 is epi & b1 is retraction & b1 is coretraction )
proof
take  idm o ; ::_thesis: ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction )
thus  ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction ) by Lm1, Th1; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
cluster retraction coretraction iso mono epi for Element of <^o,o^>;
existence
 ex b1 being Morphism of o,o st
( b1 is mono & b1 is epi & b1 is iso & b1 is retraction & b1 is coretraction )
proof
take I = idm o; ::_thesis: ( I is mono & I is epi & I is iso & I is retraction & I is coretraction )
 ( <^o,o^> <> {} & I is retraction & I is coretraction ) by Th1, ALTCAT_1:19;
hence  ( I is mono & I is epi & I is iso & I is retraction & I is coretraction ) by Th15, Th16, Th20; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
let A, B be mono Morphism of o,o;
clusterA * B ->  mono ;
coherence
 A * B is mono
proof
 <^o,o^> <> {} by ALTCAT_1:19;
hence  A * B is mono by Th9; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
let A, B be epi Morphism of o,o;
clusterA * B ->  epi ;
coherence
 A * B is epi
proof
 <^o,o^> <> {} by ALTCAT_1:19;
hence  A * B is epi by Th10; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
let A, B be iso Morphism of o,o;
clusterA * B ->  iso ;
coherence
 A * B is iso
proof
 <^o,o^> <> {} by ALTCAT_1:19;
hence  A * B is iso by Th7; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
let A, B be retraction Morphism of o,o;
clusterA * B ->  retraction ;
coherence
 A * B is retraction
proof
 <^o,o^> <> {} by ALTCAT_1:19;
hence  A * B is retraction by Th18; ::_thesis: verum
end;
end;

registration
let C be category;
let o be object of C;
let A, B be coretraction Morphism of o,o;
clusterA * B ->  coretraction ;
coherence
 A * B is coretraction
proof
 <^o,o^> <> {} by ALTCAT_1:19;
hence  A * B is coretraction by Th19; ::_thesis: verum
end;
end;

definition
let C be AltGraph ;
let o be object of C;
attro is initial  means :Def9: :: ALTCAT_3:def 9
 for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial );
end;

:: deftheorem Def9 defines initial ALTCAT_3:def_9_:_
 for C being AltGraph
for o being object of C holds
( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial ) );

theorem :: ALTCAT_3:25
for C being AltGraph
for o being object of C holds
( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
proof
let C be AltGraph ; ::_thesis: for o being object of C holds
( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
let o be object of C; ::_thesis: ( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
thus  ( o is initial implies for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) ) ::_thesis: ( ( for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) ) implies o is initial )
proof
assume A1: o is initial ; ::_thesis: for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) )
let o1 be object of C; ::_thesis: ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) )
consider M being Morphism of o,o1 such that
A2: M in <^o,o1^> and
A3: <^o,o1^> is trivial by A1, Def9;
 ex i being set st <^o,o1^> = {i} by A2, A3, ZFMISC_1:131;
then  <^o,o1^> = {M} by TARSKI:def_1;
then  for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 by TARSKI:def_1;
hence  ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) by A2; ::_thesis: verum
end;
assume A4: for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) ; ::_thesis: o is initial
let o1 be object of C; :: according to ALTCAT_3:def_9 ::_thesis: ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial )
consider M being Morphism of o,o1 such that
A5: M in <^o,o1^> and
A6: for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 by A4;
A7: <^o,o1^> c= {M}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o,o1^> or x in {M} )
assume A8: x in <^o,o1^> ; ::_thesis: x in {M}
then reconsider M1 = x as Morphism of o,o1 ;
 M1 = M by A6, A8;
hence  x in {M} by TARSKI:def_1; ::_thesis: verum
end;
 {M} c= <^o,o1^>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {M} or x in <^o,o1^> )
assume  x in {M} ; ::_thesis: x in <^o,o1^>
hence  x in <^o,o1^> by A5, TARSKI:def_1; ::_thesis: verum
end;
then  <^o,o1^> = {M} by A7, XBOOLE_0:def_10;
hence  ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial ) ; ::_thesis: verum
end;

theorem Th26: :: ALTCAT_3:26
for C being category
for o1, o2 being object of C st o1 is initial & o2 is initial holds
o1,o2 are_iso
proof
let C be category; ::_thesis: for o1, o2 being object of C st o1 is initial & o2 is initial holds
o1,o2 are_iso
let o1, o2 be object of C; ::_thesis: ( o1 is initial & o2 is initial implies o1,o2 are_iso )
assume that
A1: o1 is initial and
A2: o2 is initial ; ::_thesis: o1,o2 are_iso
 ex N being Morphism of o2,o2 st
( N in <^o2,o2^> & <^o2,o2^> is trivial ) by A2, Def9;
then consider y being set  such that
A3: <^o2,o2^> = {y} by ZFMISC_1:131;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> and
 <^o2,o1^> is trivial by A2, Def9;
consider M1 being Morphism of o1,o2 such that
A5: M1 in <^o1,o2^> and
 <^o1,o2^> is trivial by A1, Def9;
thus  ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A5, A4; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o2 st A is iso
 ( M1 * M2 = y & idm o2 = y ) by A3, TARSKI:def_1;
then  M2 is_right_inverse_of M1 by Def1;
then A6: M1 is retraction by Def2;
 ex M being Morphism of o1,o1 st
( M in <^o1,o1^> & <^o1,o1^> is trivial ) by A1, Def9;
then consider x being set  such that
A7: <^o1,o1^> = {x} by ZFMISC_1:131;
 ( M2 * M1 = x & idm o1 = x ) by A7, TARSKI:def_1;
then  M2 is_left_inverse_of M1 by Def1;
then  M1 is coretraction by Def3;
then  M1 is iso by A5, A4, A6, Th6;
hence  ex A being Morphism of o1,o2 st A is iso ; ::_thesis: verum
end;

definition
let C be AltGraph ;
let o be object of C;
attro is terminal  means :Def10: :: ALTCAT_3:def 10
 for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial );
end;

:: deftheorem Def10 defines terminal ALTCAT_3:def_10_:_
 for C being AltGraph
for o being object of C holds
( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial ) );

theorem :: ALTCAT_3:27
for C being AltGraph
for o being object of C holds
( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
proof
let C be AltGraph ; ::_thesis: for o being object of C holds
( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
let o be object of C; ::_thesis: ( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
thus  ( o is terminal implies for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ) ::_thesis: ( ( for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ) implies o is terminal )
proof
assume A1: o is terminal ; ::_thesis: for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) )
let o1 be object of C; ::_thesis: ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) )
consider M being Morphism of o1,o such that
A2: M in <^o1,o^> and
A3: <^o1,o^> is trivial by A1, Def10;
 ex i being set st <^o1,o^> = {i} by A2, A3, ZFMISC_1:131;
then  <^o1,o^> = {M} by TARSKI:def_1;
then  for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 by TARSKI:def_1;
hence  ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) by A2; ::_thesis: verum
end;
assume A4: for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ; ::_thesis: o is terminal
let o1 be object of C; :: according to ALTCAT_3:def_10 ::_thesis: ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial )
consider M being Morphism of o1,o such that
A5: M in <^o1,o^> and
A6: for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 by A4;
A7: <^o1,o^> c= {M}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o1,o^> or x in {M} )
assume A8: x in <^o1,o^> ; ::_thesis: x in {M}
then reconsider M1 = x as Morphism of o1,o ;
 M1 = M by A6, A8;
hence  x in {M} by TARSKI:def_1; ::_thesis: verum
end;
 {M} c= <^o1,o^>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {M} or x in <^o1,o^> )
assume  x in {M} ; ::_thesis: x in <^o1,o^>
hence  x in <^o1,o^> by A5, TARSKI:def_1; ::_thesis: verum
end;
then  <^o1,o^> = {M} by A7, XBOOLE_0:def_10;
hence  ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial ) ; ::_thesis: verum
end;

theorem :: ALTCAT_3:28
for C being category
for o1, o2 being object of C st o1 is terminal & o2 is terminal holds
o1,o2 are_iso
proof
let C be category; ::_thesis: for o1, o2 being object of C st o1 is terminal & o2 is terminal holds
o1,o2 are_iso
let o1, o2 be object of C; ::_thesis: ( o1 is terminal & o2 is terminal implies o1,o2 are_iso )
assume that
A1: o1 is terminal and
A2: o2 is terminal ; ::_thesis: o1,o2 are_iso
 ex M being Morphism of o1,o1 st
( M in <^o1,o1^> & <^o1,o1^> is trivial ) by A1, Def10;
then consider x being set  such that
A3: <^o1,o1^> = {x} by ZFMISC_1:131;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> and
 <^o2,o1^> is trivial by A1, Def10;
consider M1 being Morphism of o1,o2 such that
A5: M1 in <^o1,o2^> and
 <^o1,o2^> is trivial by A2, Def10;
thus  ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A5, A4; :: according to ALTCAT_3:def_6 ::_thesis: ex A being Morphism of o1,o2 st A is iso
 M2 * M1 = x by A3, TARSKI:def_1;
then  M2 * M1 = idm o1 by A3, TARSKI:def_1;
then  M2 is_left_inverse_of M1 by Def1;
then A6: M1 is coretraction by Def3;
 ex N being Morphism of o2,o2 st
( N in <^o2,o2^> & <^o2,o2^> is trivial ) by A2, Def10;
then consider y being set  such that
A7: <^o2,o2^> = {y} by ZFMISC_1:131;
 M1 * M2 = y by A7, TARSKI:def_1;
then  M1 * M2 = idm o2 by A7, TARSKI:def_1;
then  M2 is_right_inverse_of M1 by Def1;
then  M1 is retraction by Def2;
then  M1 is iso by A5, A4, A6, Th6;
hence  ex A being Morphism of o1,o2 st A is iso ; ::_thesis: verum
end;

definition
let C be AltGraph ;
let o be object of C;
attro is _zero  means :Def11: :: ALTCAT_3:def 11
( o is initial & o is terminal );
end;

:: deftheorem Def11 defines _zero ALTCAT_3:def_11_:_
 for C being AltGraph
for o being object of C holds
( o is _zero iff ( o is initial & o is terminal ) );

theorem :: ALTCAT_3:29
for C being category
for o1, o2 being object of C st o1 is _zero & o2 is _zero holds
o1,o2 are_iso
proof
let C be category; ::_thesis: for o1, o2 being object of C st o1 is _zero & o2 is _zero holds
o1,o2 are_iso
let o1, o2 be object of C; ::_thesis: ( o1 is _zero & o2 is _zero implies o1,o2 are_iso )
assume  ( o1 is _zero & o2 is _zero ) ; ::_thesis: o1,o2 are_iso
then  ( o1 is initial & o2 is initial ) by Def11;
hence  o1,o2 are_iso by Th26; ::_thesis: verum
end;

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let M be Morphism of o1,o2;
attrM is _zero  means :Def12: :: ALTCAT_3:def 12
 for o being object of C st o is _zero holds
for A being Morphism of o1,o
for B being Morphism of o,o2 holds M = B * A;
end;

:: deftheorem Def12 defines _zero ALTCAT_3:def_12_:_
 for C being non empty AltCatStr
for o1, o2 being object of C
for M being Morphism of o1,o2 holds
( M is _zero iff for o being object of C st o is _zero holds
for A being Morphism of o1,o
for B being Morphism of o,o2 holds M = B * A );

theorem :: ALTCAT_3:30
for C being category
for o1, o2, o3 being object of C
for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
proof
let C be category; ::_thesis: for o1, o2, o3 being object of C
for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let o1, o2, o3 be object of C; ::_thesis: for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let M1 be Morphism of o1,o2; ::_thesis: for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let M2 be Morphism of o2,o3; ::_thesis: ( M1 is _zero & M2 is _zero implies M2 * M1 is _zero )
assume that
A1: M1 is _zero and
A2: M2 is _zero ; ::_thesis: M2 * M1 is _zero
let o be object of C; :: according to ALTCAT_3:def_12 ::_thesis: ( o is _zero implies for A being Morphism of o1,o
for B being Morphism of o,o3 holds M2 * M1 = B * A )
assume A3: o is _zero ; ::_thesis: for A being Morphism of o1,o
for B being Morphism of o,o3 holds M2 * M1 = B * A
then A4: o is initial by Def11;
then consider B1 being Morphism of o,o2 such that
A5: B1 in <^o,o2^> and
 <^o,o2^> is trivial by Def9;
let A be Morphism of o1,o; ::_thesis: for B being Morphism of o,o3 holds M2 * M1 = B * A
let B be Morphism of o,o3; ::_thesis: M2 * M1 = B * A
consider B2 being Morphism of o,o3 such that
A6: B2 in <^o,o3^> and
A7: <^o,o3^> is trivial by A4, Def9;
consider y being set  such that
A8: <^o,o3^> = {y} by A6, A7, ZFMISC_1:131;
A9: o is terminal by A3, Def11;
then consider A1 being Morphism of o1,o such that
A10: A1 in <^o1,o^> and
A11: <^o1,o^> is trivial by Def10;
consider x being set  such that
A12: <^o1,o^> = {x} by A10, A11, ZFMISC_1:131;
 ex M being Morphism of o,o st
( M in <^o,o^> & <^o,o^> is trivial ) by A9, Def10;
then consider z being set  such that
A13: <^o,o^> = {z} by ZFMISC_1:131;
consider A2 being Morphism of o2,o such that
A14: A2 in <^o2,o^> and
 <^o2,o^> is trivial by A9, Def10;
A15: ( idm o = z & A2 * B1 = z ) by A13, TARSKI:def_1;
A16: ( B = y & B2 = y ) by A8, TARSKI:def_1;
A17: ( A = x & A1 = x ) by A12, TARSKI:def_1;
A18: <^o2,o3^> <> {} by A6, A14, ALTCAT_1:def_2;
 M2 = B2 * A2 by A2, A3, Def12;
hence M2 * M1 = (B2 * A2) * (B1 * A1) by A1, A3, Def12
.= ((B2 * A2) * B1) * A1 by A5, A10, A18, ALTCAT_1:21
.= (B * (idm o)) * A by A5, A6, A14, A17, A16, A15, ALTCAT_1:21
.= B * A by A6, ALTCAT_1:def_17 ;
::_thesis: verum
end;