:: CAT_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let I be set ;
let A be non empty set ;
let F be Function of I,A;
let x be set ;
assume A1: x in I ;
redefine func F /. x equals :Def1: :: CAT_3:def 1
F . x;
compatibility
for b1 being Element of A holds
( b1 = F /. x iff b1 = F . x )
proof end;
end;

:: deftheorem Def1 defines /. CAT_3:def 1 :
for I being set
for A being non empty set
for F being Function of I,A
for x being set st x in I holds
F /. x = F . x;

scheme :: CAT_3:sch 1
LambdaIdx{ F1() -> set , F2() -> non empty set , F3( set ) -> Element of F2() } :
ex F being Function of F1(),F2() st
for x being set st x in F1() holds
F /. x = F3(x)
proof end;

theorem Th1: :: CAT_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being non empty set
for F1, F2 being Function of I,A st ( for x being set st x in I holds
F1 /. x = F2 /. x ) holds
F1 = F2
proof end;

scheme :: CAT_3:sch 2
FuncIdxcorrectness{ F1() -> set , F2() -> non empty set , F3( set ) -> Element of F2() } :
( ex F being Function of F1(),F2() st
for x being set st x in F1() holds
F /. x = F3(x) & ( for F1, F2 being Function of F1(),F2() st ( for x being set st x in F1() holds
F1 /. x = F3(x) ) & ( for x being set st x in F1() holds
F2 /. x = F3(x) ) holds
F1 = F2 ) )
proof end;

definition
let A be non empty set ;
let I be set ;
let a be Element of A;
:: original: -->
redefine func I --> a -> Function of I,A;
coherence
I --> a is Function of I,A
by FUNCOP_1:58;
end;

definition
let A be non empty set ;
let x be set ;
let a be Element of A;
:: original: .-->
redefine func x .--> a -> Function of {x},A;
coherence
x .--> a is Function of {x},A
by FUNCOP_1:58;
end;

theorem Th2: :: CAT_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set
for A being non empty set
for a being Element of A st x in I holds
(I --> a) /. x = a
proof end;

theorem :: CAT_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CAT_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: CAT_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for A being non empty set st x1 <> x2 holds
for y1, y2 being Element of A holds
( (x1,x2 --> y1,y2) /. x1 = y1 & (x1,x2 --> y1,y2) /. x2 = y2 )
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I,the Morphisms of C;
canceled;
func doms F -> Function of I,the Objects of C means :Def3: :: CAT_3:def 3
for x being set st x in I holds
it /. x = dom (F /. x);
correctness
existence
ex b1 being Function of I,the Objects of C st
for x being set st x in I holds
b1 /. x = dom (F /. x)
;
uniqueness
for b1, b2 being Function of I,the Objects of C st ( for x being set st x in I holds
b1 /. x = dom (F /. x) ) & ( for x being set st x in I holds
b2 /. x = dom (F /. x) ) holds
b1 = b2
;
proof end;
func cods F -> Function of I,the Objects of C means :Def4: :: CAT_3:def 4
for x being set st x in I holds
it /. x = cod (F /. x);
correctness
existence
ex b1 being Function of I,the Objects of C st
for x being set st x in I holds
b1 /. x = cod (F /. x)
;
uniqueness
for b1, b2 being Function of I,the Objects of C st ( for x being set st x in I holds
b1 /. x = cod (F /. x) ) & ( for x being set st x in I holds
b2 /. x = cod (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem CAT_3:def 2 :
canceled;

:: deftheorem Def3 defines doms CAT_3:def 3 :
for C being Category
for I being set
for F being Function of I,the Morphisms of C
for b4 being Function of I,the Objects of C holds
( b4 = doms F iff for x being set st x in I holds
b4 /. x = dom (F /. x) );

:: deftheorem Def4 defines cods CAT_3:def 4 :
for C being Category
for I being set
for F being Function of I,the Morphisms of C
for b4 being Function of I,the Objects of C holds
( b4 = cods F iff for x being set st x in I holds
b4 /. x = cod (F /. x) );

theorem Th8: :: CAT_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C holds doms (I --> f) = I --> (dom f)
proof end;

theorem Th9: :: CAT_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C holds cods (I --> f) = I --> (cod f)
proof end;

theorem Th10: :: CAT_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2)
proof end;

theorem Th11: :: CAT_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds cods (x1,x2 --> p1,p2) = x1,x2 --> (cod p1),(cod p2)
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I,the Morphisms of C;
func F opp -> Function of I,the Morphisms of (C opp ) means :Def5: :: CAT_3:def 5
for x being set st x in I holds
it /. x = (F /. x) opp ;
correctness
existence
ex b1 being Function of I,the Morphisms of (C opp ) st
for x being set st x in I holds
b1 /. x = (F /. x) opp
;
uniqueness
for b1, b2 being Function of I,the Morphisms of (C opp ) st ( for x being set st x in I holds
b1 /. x = (F /. x) opp ) & ( for x being set st x in I holds
b2 /. x = (F /. x) opp ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines opp CAT_3:def 5 :
for C being Category
for I being set
for F being Function of I,the Morphisms of C
for b4 being Function of I,the Morphisms of (C opp ) holds
( b4 = F opp iff for x being set st x in I holds
b4 /. x = (F /. x) opp );

theorem :: CAT_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C holds (I --> f) opp = I --> (f opp )
proof end;

theorem :: CAT_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp )
proof end;

theorem :: CAT_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for F being Function of I,the Morphisms of C holds (F opp ) opp = F
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I,the Morphisms of (C opp );
func opp F -> Function of I,the Morphisms of C means :Def6: :: CAT_3:def 6
for x being set st x in I holds
it /. x = opp (F /. x);
correctness
existence
ex b1 being Function of I,the Morphisms of C st
for x being set st x in I holds
b1 /. x = opp (F /. x)
;
uniqueness
for b1, b2 being Function of I,the Morphisms of C st ( for x being set st x in I holds
b1 /. x = opp (F /. x) ) & ( for x being set st x in I holds
b2 /. x = opp (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def6 defines opp CAT_3:def 6 :
for C being Category
for I being set
for F being Function of I,the Morphisms of (C opp )
for b4 being Function of I,the Morphisms of C holds
( b4 = opp F iff for x being set st x in I holds
b4 /. x = opp (F /. x) );

theorem :: CAT_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of (C opp ) holds opp (I --> f) = I --> (opp f)
proof end;

theorem :: CAT_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category st x1 <> x2 holds
for p1, p2 being Morphism of (C opp ) holds opp (x1,x2 --> p1,p2) = x1,x2 --> (opp p1),(opp p2)
proof end;

theorem :: CAT_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for F being Function of I,the Morphisms of C holds opp (F opp ) = F
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I,the Morphisms of C;
let f be Morphism of C;
func F * f -> Function of I,the Morphisms of C means :Def7: :: CAT_3:def 7
for x being set st x in I holds
it /. x = (F /. x) * f;
correctness
existence
ex b1 being Function of I,the Morphisms of C st
for x being set st x in I holds
b1 /. x = (F /. x) * f
;
uniqueness
for b1, b2 being Function of I,the Morphisms of C st ( for x being set st x in I holds
b1 /. x = (F /. x) * f ) & ( for x being set st x in I holds
b2 /. x = (F /. x) * f ) holds
b1 = b2
;
proof end;
func f * F -> Function of I,the Morphisms of C means :Def8: :: CAT_3:def 8
for x being set st x in I holds
it /. x = f * (F /. x);
correctness
existence
ex b1 being Function of I,the Morphisms of C st
for x being set st x in I holds
b1 /. x = f * (F /. x)
;
uniqueness
for b1, b2 being Function of I,the Morphisms of C st ( for x being set st x in I holds
b1 /. x = f * (F /. x) ) & ( for x being set st x in I holds
b2 /. x = f * (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines * CAT_3:def 7 :
for C being Category
for I being set
for F being Function of I,the Morphisms of C
for f being Morphism of C
for b5 being Function of I,the Morphisms of C holds
( b5 = F * f iff for x being set st x in I holds
b5 /. x = (F /. x) * f );

:: deftheorem Def8 defines * CAT_3:def 8 :
for C being Category
for I being set
for F being Function of I,the Morphisms of C
for f being Morphism of C
for b5 being Function of I,the Morphisms of C holds
( b5 = f * F iff for x being set st x in I holds
b5 /. x = f * (F /. x) );

theorem Th18: :: CAT_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for p1, p2, f being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) * f = x1,x2 --> (p1 * f),(p2 * f)
proof end;

theorem Th19: :: CAT_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for f, p1, p2 being Morphism of C st x1 <> x2 holds
f * (x1,x2 --> p1,p2) = x1,x2 --> (f * p1),(f * p2)
proof end;

theorem Th20: :: CAT_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Function of I,the Morphisms of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
proof end;

theorem Th21: :: CAT_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Function of I,the Morphisms of C st cods F = I --> (dom f) holds
( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )
proof end;

definition
let C be Category;
let I be set ;
let F, G be Function of I,the Morphisms of C;
func F "*" G -> Function of I,the Morphisms of C means :Def9: :: CAT_3:def 9
for x being set st x in I holds
it /. x = (F /. x) * (G /. x);
correctness
existence
ex b1 being Function of I,the Morphisms of C st
for x being set st x in I holds
b1 /. x = (F /. x) * (G /. x)
;
uniqueness
for b1, b2 being Function of I,the Morphisms of C st ( for x being set st x in I holds
b1 /. x = (F /. x) * (G /. x) ) & ( for x being set st x in I holds
b2 /. x = (F /. x) * (G /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def9 defines "*" CAT_3:def 9 :
for C being Category
for I being set
for F, G, b5 being Function of I,the Morphisms of C holds
( b5 = F "*" G iff for x being set st x in I holds
b5 /. x = (F /. x) * (G /. x) );

theorem Th22: :: CAT_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for F, G being Function of I,the Morphisms of C st doms F = cods G holds
( doms (F "*" G) = doms G & cods (F "*" G) = cods F )
proof end;

theorem :: CAT_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) "*" (x1,x2 --> q1,q2) = x1,x2 --> (p1 * q1),(p2 * q2)
proof end;

theorem :: CAT_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Function of I,the Morphisms of C holds F * f = F "*" (I --> f)
proof end;

theorem :: CAT_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Function of I,the Morphisms of C holds f * F = (I --> f) "*" F
proof end;

definition
let C be Category;
let IT be Morphism of C;
attr IT is retraction means :Def10: :: CAT_3:def 10
ex g being Morphism of C st
( cod g = dom IT & IT * g = id (cod IT) );
attr IT is coretraction means :Def11: :: CAT_3:def 11
ex g being Morphism of C st
( dom g = cod IT & g * IT = id (dom IT) );
end;

:: deftheorem Def10 defines retraction CAT_3:def 10 :
for C being Category
for IT being Morphism of C holds
( IT is retraction iff ex g being Morphism of C st
( cod g = dom IT & IT * g = id (cod IT) ) );

:: deftheorem Def11 defines coretraction CAT_3:def 11 :
for C being Category
for IT being Morphism of C holds
( IT is coretraction iff ex g being Morphism of C st
( dom g = cod IT & g * IT = id (dom IT) ) );

theorem Th26: :: CAT_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C st f is retraction holds
f is epi
proof end;

theorem :: CAT_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C st f is coretraction holds
f is monic
proof end;

theorem :: CAT_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C st f is retraction & g is retraction & dom g = cod f holds
g * f is retraction
proof end;

theorem :: CAT_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C st f is coretraction & g is coretraction & dom g = cod f holds
g * f is coretraction
proof end;

theorem :: CAT_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for g, f being Morphism of C st dom g = cod f & g * f is retraction holds
g is retraction
proof end;

theorem :: CAT_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for g, f being Morphism of C st dom g = cod f & g * f is coretraction holds
f is coretraction
proof end;

theorem :: CAT_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C st f is retraction & f is monic holds
f is invertible
proof end;

theorem Th33: :: CAT_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C st f is coretraction & f is epi holds
f is invertible
proof end;

theorem :: CAT_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f is invertible iff ( f is retraction & f is coretraction ) )
proof end;

theorem :: CAT_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for T being Functor of C,D st f is retraction holds
T . f is retraction
proof end;

theorem :: CAT_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Category
for f being Morphism of C
for T being Functor of C,D st f is coretraction holds
T . f is coretraction
proof end;

theorem :: CAT_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f is retraction iff f opp is coretraction )
proof end;

theorem :: CAT_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f being Morphism of C holds
( f is coretraction iff f opp is retraction )
proof end;

definition
let C be Category;
let a, b be Object of C;
assume A1: b is terminal ;
func term a,b -> Morphism of a,b means :: CAT_3:def 12
verum;
existence
ex b1 being Morphism of a,b st verum
;
uniqueness
for b1, b2 being Morphism of a,b holds b1 = b2
proof end;
end;

:: deftheorem defines term CAT_3:def 12 :
for C being Category
for a, b being Object of C st b is terminal holds
for b4 being Morphism of a,b holds
( b4 = term a,b iff verum );

theorem Th39: :: CAT_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for b, a being Object of C st b is terminal holds
( dom (term a,b) = a & cod (term a,b) = b )
proof end;

theorem Th40: :: CAT_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for b, a being Object of C
for f being Morphism of C st b is terminal & dom f = a & cod f = b holds
term a,b = f
proof end;

theorem :: CAT_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C
for f being Morphism of a,b st b is terminal holds
term a,b = f
proof end;

definition
let C be Category;
let a, b be Object of C;
assume A1: a is initial ;
func init a,b -> Morphism of a,b means :: CAT_3:def 13
verum;
existence
ex b1 being Morphism of a,b st verum
;
uniqueness
for b1, b2 being Morphism of a,b holds b1 = b2
proof end;
end;

:: deftheorem defines init CAT_3:def 13 :
for C being Category
for a, b being Object of C st a is initial holds
for b4 being Morphism of a,b holds
( b4 = init a,b iff verum );

theorem Th42: :: CAT_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C st a is initial holds
( dom (init a,b) = a & cod (init a,b) = b )
proof end;

theorem Th43: :: CAT_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C
for f being Morphism of C st a is initial & dom f = a & cod f = b holds
init a,b = f
proof end;

theorem :: CAT_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C
for f being Morphism of a,b st a is initial holds
init a,b = f
proof end;

definition
let C be Category;
let a be Object of C;
let I be set ;
mode Projections_family of a,I -> Function of I,the Morphisms of C means :Def14: :: CAT_3:def 14
doms it = I --> a;
existence
ex b1 being Function of I,the Morphisms of C st doms b1 = I --> a
proof end;
end;

:: deftheorem Def14 defines Projections_family CAT_3:def 14 :
for C being Category
for a being Object of C
for I being set
for b4 being Function of I,the Morphisms of C holds
( b4 is Projections_family of a,I iff doms b4 = I --> a );

theorem Th45: :: CAT_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a
proof end;

theorem Th46: :: CAT_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for F being Function of {} ,the Morphisms of C holds F is Projections_family of a, {}
proof end;

theorem Th47: :: CAT_3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for C being Category
for a being Object of C
for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}
proof end;

theorem Th48: :: CAT_3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
x1,x2 --> p1,p2 is Projections_family of a,{x1,x2}
proof end;

theorem :: CAT_3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th50: :: CAT_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a being Object of C
for f being Morphism of C
for F being Projections_family of a,I st cod f = a holds
F * f is Projections_family of dom f,I
proof end;

theorem :: CAT_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a being Object of C
for F being Function of I,the Morphisms of C
for G being Projections_family of a,I st doms F = cods G holds
F "*" G is Projections_family of a,I
proof end;

theorem :: CAT_3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Projections_family of cod f,I holds (f opp ) * (F opp ) = (F * f) opp
proof end;

definition
let C be Category;
let a be Object of C;
let I be set ;
let F be Function of I,the Morphisms of C;
pred a is_a_product_wrt F means :Def15: :: CAT_3:def 15
( F is Projections_family of a,I & ( for b being Object of C
for F' being Projections_family of b,I st cods F = cods F' holds
ex h being Morphism of C st
( h in Hom b,a & ( for k being Morphism of C st k in Hom b,a holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) ) ) );
end;

:: deftheorem Def15 defines is_a_product_wrt CAT_3:def 15 :
for C being Category
for a being Object of C
for I being set
for F being Function of I,the Morphisms of C holds
( a is_a_product_wrt F iff ( F is Projections_family of a,I & ( for b being Object of C
for F' being Projections_family of b,I st cods F = cods F' holds
ex h being Morphism of C st
( h in Hom b,a & ( for k being Morphism of C st k in Hom b,a holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff h = k ) ) ) ) ) );

theorem Th53: :: CAT_3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c, d being Object of C
for F being Projections_family of c,I
for F' being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' holds
c,d are_isomorphic
proof end;

theorem Th54: :: CAT_3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c being Object of C
for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom (cod (F /. x1)),(cod (F /. x2)) <> {} ) holds
for x being set st x in I holds
F /. x is retraction
proof end;

theorem Th55: :: CAT_3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for F being Function of {} ,the Morphisms of C holds
( a is_a_product_wrt F iff a is terminal )
proof end;

theorem Th56: :: CAT_3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a, b being Object of C
for f being Morphism of C
for F being Projections_family of a,I st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
proof end;

theorem :: CAT_3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for C being Category
for a being Object of C holds a is_a_product_wrt y .--> (id a)
proof end;

theorem :: CAT_3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal
proof end;

definition
let C be Category;
let c be Object of C;
let p1, p2 be Morphism of C;
pred c is_a_product_wrt p1,p2 means :Def16: :: CAT_3:def 16
( dom p1 = c & dom p2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom d,(cod p1) & g in Hom d,(cod p2) holds
ex h being Morphism of C st
( h in Hom d,c & ( for k being Morphism of C st k in Hom d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ) );
end;

:: deftheorem Def16 defines is_a_product_wrt CAT_3:def 16 :
for C being Category
for c being Object of C
for p1, p2 being Morphism of C holds
( c is_a_product_wrt p1,p2 iff ( dom p1 = c & dom p2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom d,(cod p1) & g in Hom d,(cod p2) holds
ex h being Morphism of C st
( h in Hom d,c & ( for k being Morphism of C st k in Hom d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ) ) );

theorem Th59: :: CAT_3:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt x1,x2 --> p1,p2 )
proof end;

theorem :: CAT_3:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, a, b being Object of C st Hom c,a <> {} & Hom c,b <> {} holds
for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
proof end;

theorem :: CAT_3:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, d being Object of C
for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds
c,d are_isomorphic
proof end;

theorem :: CAT_3:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & Hom (cod p1),(cod p2) <> {} & Hom (cod p2),(cod p1) <> {} holds
( p1 is retraction & p2 is retraction )
proof end;

theorem Th63: :: CAT_3:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for p1, p2, h being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom c,c & p1 * h = p1 & p2 * h = p2 holds
h = id c
proof end;

theorem :: CAT_3:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, d being Object of C
for p1, p2, f being Morphism of C st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 * f,p2 * f
proof end;

theorem :: CAT_3:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds
c, cod p1 are_isomorphic
proof end;

theorem :: CAT_3:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds
c, cod p2 are_isomorphic
proof end;

definition
let C be Category;
let c be Object of C;
let I be set ;
mode Injections_family of c,I -> Function of I,the Morphisms of C means :Def17: :: CAT_3:def 17
cods it = I --> c;
existence
ex b1 being Function of I,the Morphisms of C st cods b1 = I --> c
proof end;
end;

:: deftheorem Def17 defines Injections_family CAT_3:def 17 :
for C being Category
for c being Object of C
for I being set
for b4 being Function of I,the Morphisms of C holds
( b4 is Injections_family of c,I iff cods b4 = I --> c );

theorem Th67: :: CAT_3:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st x in I holds
cod (F /. x) = c
proof end;

theorem :: CAT_3:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for F being Function of {} ,the Morphisms of C holds F is Injections_family of a, {}
proof end;

theorem Th69: :: CAT_3:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for C being Category
for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}
proof end;

theorem Th70: :: CAT_3:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds
x1,x2 --> p1,p2 is Injections_family of c,{x1,x2}
proof end;

theorem :: CAT_3:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th72: :: CAT_3:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for b being Object of C
for f being Morphism of C
for F being Injections_family of b,I st dom f = b holds
f * F is Injections_family of cod f,I
proof end;

theorem :: CAT_3:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for b being Object of C
for F being Injections_family of b,I
for G being Function of I,the Morphisms of C st doms F = cods G holds
F "*" G is Injections_family of b,I
proof end;

theorem Th74: :: CAT_3:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c being Object of C
for F being Function of I,the Morphisms of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
proof end;

theorem Th75: :: CAT_3:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for F being Function of I,the Morphisms of (C opp )
for c being Object of (C opp ) holds
( F is Injections_family of c,I iff opp F is Projections_family of opp c,I )
proof end;

theorem :: CAT_3:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for f being Morphism of C
for F being Injections_family of dom f,I holds (F opp ) * (f opp ) = (f * F) opp
proof end;

definition
let C be Category;
let c be Object of C;
let I be set ;
let F be Function of I,the Morphisms of C;
pred c is_a_coproduct_wrt F means :Def18: :: CAT_3:def 18
( F is Injections_family of c,I & ( for d being Object of C
for F' being Injections_family of d,I st doms F = doms F' holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( for x being set st x in I holds
k * (F /. x) = F' /. x ) iff h = k ) ) ) ) );
end;

:: deftheorem Def18 defines is_a_coproduct_wrt CAT_3:def 18 :
for C being Category
for c being Object of C
for I being set
for F being Function of I,the Morphisms of C holds
( c is_a_coproduct_wrt F iff ( F is Injections_family of c,I & ( for d being Object of C
for F' being Injections_family of d,I st doms F = doms F' holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( for x being set st x in I holds
k * (F /. x) = F' /. x ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c being Object of C
for F being Function of I,the Morphisms of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
proof end;

theorem Th78: :: CAT_3:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c, d being Object of C
for F being Injections_family of c,I
for F' being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F' & doms F = doms F' holds
c,d are_isomorphic
proof end;

theorem Th79: :: CAT_3:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom (dom (F /. x1)),(dom (F /. x2)) <> {} ) holds
for x being set st x in I holds
F /. x is coretraction
proof end;

theorem Th80: :: CAT_3:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a, b being Object of C
for f being Morphism of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
proof end;

theorem Th81: :: CAT_3:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )
proof end;

theorem :: CAT_3:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for C being Category
for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)
proof end;

theorem :: CAT_3:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for C being Category
for a being Object of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial
proof end;

definition
let C be Category;
let c be Object of C;
let i1, i2 be Morphism of C;
pred c is_a_coproduct_wrt i1,i2 means :Def19: :: CAT_3:def 19
( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom (dom i1),d & g in Hom (dom i2),d holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) ) );
end;

:: deftheorem Def19 defines is_a_coproduct_wrt CAT_3:def 19 :
for C being Category
for c being Object of C
for i1, i2 being Morphism of C holds
( c is_a_coproduct_wrt i1,i2 iff ( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom (dom i1),d & g in Hom (dom i2),d holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for p1, p2 being Morphism of C holds
( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )
proof end;

theorem Th85: :: CAT_3:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt x1,x2 --> i1,i2 )
proof end;

theorem :: CAT_3:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, d being Object of C
for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds
c,d are_isomorphic
proof end;

theorem :: CAT_3:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, c, b being Object of C st Hom a,c <> {} & Hom b,c <> {} holds
for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom a,d <> {} & Hom b,d <> {} holds
( Hom c,d <> {} & ( for f being Morphism of a,d
for g being Morphism of b,d ex h being Morphism of c,d st
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) )
proof end;

theorem :: CAT_3:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & Hom (dom i1),(dom i2) <> {} & Hom (dom i2),(dom i1) <> {} holds
( i1 is coretraction & i2 is coretraction )
proof end;

theorem Th89: :: CAT_3:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom c,c & h * i1 = i1 & h * i2 = i2 holds
h = id c
proof end;

theorem :: CAT_3:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, d being Object of C
for i1, i2, f being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f * i1,f * i2
proof end;

theorem :: CAT_3:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds
dom i1,c are_isomorphic
proof end;

theorem :: CAT_3:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i1 is initial holds
dom i2,c are_isomorphic
proof end;