:: by Maciej Goli\'nski and Artur Korni{\l}owicz

::

:: Received December 8, 2013

:: Copyright (c) 2013-2021 Association of Mizar Users

set C = EnsCat {{}};

Lm1: the carrier of (EnsCat {{}}) = {0}

by ALTCAT_1:def 14;

Lm2: Funcs ({},{}) = {{}}

by FUNCT_5:57;

Lm3: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds

( {} is Morphism of o1,o & {} in <^o1,o^> )

( {} is Morphism of o1,o & {} in <^o1,o^> )

let o1, o be Object of (EnsCat {{}}); :: thesis: ( {} is Morphism of o1,o & {} in <^o1,o^> )

A1: ( o1 = {} & o = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence ( {} is Morphism of o1,o & {} in <^o1,o^> ) by A1, Lm1, Lm2; :: thesis: verum

end;
A1: ( o1 = {} & o = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence ( {} is Morphism of o1,o & {} in <^o1,o^> ) by A1, Lm1, Lm2; :: thesis: verum

Lm4: now :: thesis: for o1, o being Object of (EnsCat {{}})

for m1 being Morphism of o1,o holds m1 = {}

for m1 being Morphism of o1,o holds m1 = {}

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1 being Morphism of o1,o holds m1 = {}

let m1 be Morphism of o1,o; :: thesis: m1 = {}

A1: ( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence m1 = {} by A1, Lm2, TARSKI:def 1; :: thesis: verum

end;
let m1 be Morphism of o1,o; :: thesis: m1 = {}

A1: ( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

<^o1,o^> = Funcs (o1,o) by ALTCAT_1:def 14;

hence m1 = {} by A1, Lm2, TARSKI:def 1; :: thesis: verum

Lm5: now :: thesis: for o1, o being Object of (EnsCat {{}}) holds o1 = o

let o1, o be Object of (EnsCat {{}}); :: thesis: o1 = o

( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

hence o1 = o ; :: thesis: verum

end;
( o = {} & o1 = {} ) by Lm1, TARSKI:def 1;

hence o1 = o ; :: thesis: verum

Lm6: now :: thesis: for o1, o being Object of (EnsCat {{}})

for m1, m being Morphism of o1,o holds m1 = m

for m1, m being Morphism of o1,o holds m1 = m

let o1, o be Object of (EnsCat {{}}); :: thesis: for m1, m being Morphism of o1,o holds m1 = m

let m1, m be Morphism of o1,o; :: thesis: m1 = m

thus m1 = {} by Lm4

.= m by Lm4 ; :: thesis: verum

end;
let m1, m be Morphism of o1,o; :: thesis: m1 = m

thus m1 = {} by Lm4

.= m by Lm4 ; :: thesis: verum

registration

let I be non empty set ;

let A be ManySortedSet of I;

let i be Element of I;

coherence

( coprod (i,A) is Relation-like & coprod (i,A) is Function-like )

end;
let A be ManySortedSet of I;

let i be Element of I;

coherence

( coprod (i,A) is Relation-like & coprod (i,A) is Function-like )

proof end;

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b_{1} . i is Morphism of o1,o )

end;
let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

mode MorphismsFamily of f,o -> ManySortedSet of I means :Def1: :: ALTCAT_6:def 1

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & it . i is Morphism of o1,o );

existence for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & it . i is Morphism of o1,o );

ex b

for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b

proof end;

:: deftheorem Def1 defines MorphismsFamily ALTCAT_6:def 1 :

for C being non empty AltCatStr

for o being Object of C

for I being set

for f being ObjectsFamily of I,C

for b_{5} being ManySortedSet of I holds

( b_{5} is MorphismsFamily of f,o iff for i being object st i in I holds

ex o1 being Object of C st

( o1 = f . i & b_{5} . i is Morphism of o1,o ) );

for C being non empty AltCatStr

for o being Object of C

for I being set

for f being ObjectsFamily of I,C

for b

( b

ex o1 being Object of C st

( o1 = f . i & b

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

for b_{1} being ManySortedSet of I holds

( b_{1} is MorphismsFamily of f,o iff for i being Element of I holds b_{1} . i is Morphism of (f . i),o )

end;
let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

redefine mode MorphismsFamily of f,o means :Def2: :: ALTCAT_6:def 2

for i being Element of I holds it . i is Morphism of (f . i),o;

compatibility for i being Element of I holds it . i is Morphism of (f . i),o;

for b

( b

proof end;

:: deftheorem Def2 defines MorphismsFamily ALTCAT_6:def 2 :

for C being non empty AltCatStr

for o being Object of C

for I being non empty set

for f being ObjectsFamily of I,C

for b_{5} being ManySortedSet of I holds

( b_{5} is MorphismsFamily of f,o iff for i being Element of I holds b_{5} . i is Morphism of (f . i),o );

for C being non empty AltCatStr

for o being Object of C

for I being non empty set

for f being ObjectsFamily of I,C

for b

( b

definition

let C be non empty AltCatStr ;

let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

let M be MorphismsFamily of f,o;

let i be Element of I;

:: original: .

redefine func M . i -> Morphism of (f . i),o;

coherence

M . i is Morphism of (f . i),o by Def2;

end;
let o be Object of C;

let I be non empty set ;

let f be ObjectsFamily of I,C;

let M be MorphismsFamily of f,o;

let i be Element of I;

:: original: .

redefine func M . i -> Morphism of (f . i),o;

coherence

M . i is Morphism of (f . i),o by Def2;

registration

let C be non empty functional AltCatStr ;

let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

coherence

for b_{1} being MorphismsFamily of f,o holds b_{1} is Function-yielding

end;
let o be Object of C;

let I be set ;

let f be ObjectsFamily of I,C;

coherence

for b

proof end;

theorem Th1: :: ALTCAT_6:1

for C being non empty AltCatStr

for o being Object of C

for f being ObjectsFamily of {},C holds {} is MorphismsFamily of f,o

for o being Object of C

for f being ObjectsFamily of {},C holds {} is MorphismsFamily of f,o

proof end;

definition

let C be non empty AltCatStr ;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

:: deftheorem defines feasible ALTCAT_6:def 3 :

for C being non empty AltCatStr

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is feasible iff for i being set st i in I holds

ex o being Object of C st

( o = A . i & P . i in <^o,B^> ) );

for C being non empty AltCatStr

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is feasible iff for i being set st i in I holds

ex o being Object of C st

( o = A . i & P . i in <^o,B^> ) );

definition

let C be non empty AltCatStr ;

let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> )

end;
let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

redefine attr P is feasible means :Def4: :: ALTCAT_6:def 4

for i being Element of I holds P . i in <^(A . i),B^>;

compatibility for i being Element of I holds P . i in <^(A . i),B^>;

( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> )

proof end;

:: deftheorem Def4 defines feasible ALTCAT_6:def 4 :

for C being non empty AltCatStr

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> );

for C being non empty AltCatStr

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is feasible iff for i being Element of I holds P . i in <^(A . i),B^> );

definition

let C be category;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

attr P is coprojection-morphisms means :: ALTCAT_6:def 5

for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds

f = f1 ) );

for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds

f = f1 ) );

:: deftheorem defines coprojection-morphisms ALTCAT_6:def 5 :

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds

f = f1 ) ) );

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f * Pi ) ) & ( for f1 being Morphism of B,X st ( for i being set st i in I holds

ex si being Object of C ex Pi being Morphism of si,B st

( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds

f = f1 ) ) );

definition

let C be category;

let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

compatibility

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) ) );

end;
let I be non empty set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

let P be MorphismsFamily of A,B;

redefine attr P is coprojection-morphisms means :: ALTCAT_6:def 6

for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) );

correctness for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) );

compatibility

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) ) );

proof end;

:: deftheorem defines coprojection-morphisms ALTCAT_6:def 6 :

for C being category

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) ) );

for C being category

for I being non empty set

for A being ObjectsFamily of I,C

for B being Object of C

for P being MorphismsFamily of A,B holds

( P is coprojection-morphisms iff for X being Object of C

for F being MorphismsFamily of A,X st F is feasible holds

ex f being Morphism of B,X st

( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds

f = f1 ) ) );

registration

let C be category;

let A be ObjectsFamily of {},C;

let B be Object of C;

coherence

for b_{1} being MorphismsFamily of A,B holds b_{1} is feasible
;

end;
let A be ObjectsFamily of {},C;

let B be Object of C;

coherence

for b

theorem Th2: :: ALTCAT_6:2

for C being category

for A being ObjectsFamily of {},C

for B being Object of C st B is initial holds

ex P being MorphismsFamily of A,B st

( P is empty & P is coprojection-morphisms )

for A being ObjectsFamily of {},C

for B being Object of C st B is initial holds

ex P being MorphismsFamily of A,B st

( P is empty & P is coprojection-morphisms )

proof end;

theorem Th3: :: ALTCAT_6:3

for I being set

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}}) holds I --> {} is MorphismsFamily of A,o

proof end;

theorem Th4: :: ALTCAT_6:4

for I being set

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}})

for P being MorphismsFamily of A,o st P = I --> {} holds

( P is feasible & P is coprojection-morphisms )

for A being ObjectsFamily of I,(EnsCat {{}})

for o being Object of (EnsCat {{}})

for P being MorphismsFamily of A,o st P = I --> {} holds

( P is feasible & P is coprojection-morphisms )

proof end;

definition

let C be category;

end;
attr C is with_coproducts means :Def7: :: ALTCAT_6:def 7

for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms );

for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms );

:: deftheorem Def7 defines with_coproducts ALTCAT_6:def 7 :

for C being category holds

( C is with_coproducts iff for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms ) );

for C being category holds

( C is with_coproducts iff for I being set

for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms ) );

registration
end;

registration

existence

ex b_{1} being category st

( b_{1} is with_products & b_{1} is with_coproducts & b_{1} is strict )

end;
ex b

( b

proof end;

definition

let C be category;

let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

end;
let I be set ;

let A be ObjectsFamily of I,C;

let B be Object of C;

attr B is A -CatCoproduct-like means :: ALTCAT_6:def 8

ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms );

ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms );

:: deftheorem defines -CatCoproduct-like ALTCAT_6:def 8 :

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C holds

( B is A -CatCoproduct-like iff ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms ) );

for C being category

for I being set

for A being ObjectsFamily of I,C

for B being Object of C holds

( B is A -CatCoproduct-like iff ex P being MorphismsFamily of A,B st

( P is feasible & P is coprojection-morphisms ) );

registration

let C be with_coproducts category;

let I be set ;

let A be ObjectsFamily of I,C;

existence

ex b_{1} being Object of C st b_{1} is A -CatCoproduct-like

end;
let I be set ;

let A be ObjectsFamily of I,C;

existence

ex b

proof end;

registration

let C be category;

let A be ObjectsFamily of {},C;

coherence

for b_{1} being Object of C st b_{1} is A -CatCoproduct-like holds

b_{1} is initial

end;
let A be ObjectsFamily of {},C;

coherence

for b

b

proof end;

theorem :: ALTCAT_6:5

for C being category

for A being ObjectsFamily of {},C

for B being Object of C st B is initial holds

B is A -CatCoproduct-like

for A being ObjectsFamily of {},C

for B being Object of C st B is initial holds

B is A -CatCoproduct-like

proof end;

theorem :: ALTCAT_6:6

for I being set

for C being category

for A being ObjectsFamily of I,C

for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds

C1,C2 are_iso

for C being category

for A being ObjectsFamily of I,C

for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds

C1,C2 are_iso

proof end;

definition

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: Union (coprod A) in E ;

coherence

Union (coprod A) is Object of (EnsCat E) by A1, ALTCAT_1:def 14;

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: Union (coprod A) in E ;

coherence

Union (coprod A) is Object of (EnsCat E) by A1, ALTCAT_1:def 14;

:: deftheorem Def9 defines EnsCatCoproductObj ALTCAT_6:def 9 :

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproductObj A = Union (coprod A);

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproductObj A = Union (coprod A);

definition

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b_{1} . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) )

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b_{1} . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) ) ) & ( for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b_{2} . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) ) ) holds

b_{1} = b_{2}

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

func Coprod A -> ManySortedSet of I means :Def10: :: ALTCAT_6:def 10

for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( it . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) );

existence for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( it . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) );

ex b

for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b

F . x = [x,i] ) )

proof end;

uniqueness for b

ex F being Function of (A . i),(Union (coprod A)) st

( b

F . x = [x,i] ) ) ) & ( for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b

F . x = [x,i] ) ) ) holds

b

proof end;

:: deftheorem Def10 defines Coprod ALTCAT_6:def 10 :

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E)

for b_{4} being ManySortedSet of I holds

( b_{4} = Coprod A iff for i being object st i in I holds

ex F being Function of (A . i),(Union (coprod A)) st

( b_{4} . i = F & ( for x being object st x in A . i holds

F . x = [x,i] ) ) );

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E)

for b

( b

ex F being Function of (A . i),(Union (coprod A)) st

( b

F . x = [x,i] ) ) );

registration

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

coherence

Coprod A is Function-yielding

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

coherence

Coprod A is Function-yielding

proof end;

definition

let I be set ;

let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: Union (coprod A) in E ;

Coprod A is MorphismsFamily of A, EnsCatCoproductObj A

end;
let E be non empty set ;

let A be ObjectsFamily of I,(EnsCat E);

assume A1: Union (coprod A) in E ;

func EnsCatCoproduct A -> MorphismsFamily of A, EnsCatCoproductObj A equals :Def11: :: ALTCAT_6:def 11

Coprod A;

coherence Coprod A;

Coprod A is MorphismsFamily of A, EnsCatCoproductObj A

proof end;

:: deftheorem Def11 defines EnsCatCoproduct ALTCAT_6:def 11 :

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproduct A = Coprod A;

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproduct A = Coprod A;

theorem Th7: :: ALTCAT_6:7

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds

Coprod A is V6()

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds

Coprod A is V6()

proof end;

theorem Th8: :: ALTCAT_6:8

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds

A is V6()

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) = {} holds

A is V6()

proof end;

theorem :: ALTCAT_6:9

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E & Union (coprod A) = {} holds

EnsCatCoproduct A = I --> {}

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E & Union (coprod A) = {} holds

EnsCatCoproduct A = I --> {}

proof end;

theorem Th10: :: ALTCAT_6:10

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms )

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

( EnsCatCoproduct A is feasible & EnsCatCoproduct A is coprojection-morphisms )

proof end;

theorem :: ALTCAT_6:11

for I being set

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproductObj A is A -CatCoproduct-like

for E being non empty set

for A being ObjectsFamily of I,(EnsCat E) st Union (coprod A) in E holds

EnsCatCoproductObj A is A -CatCoproduct-like

proof end;

theorem :: ALTCAT_6:12

for E being non empty set st ( for I being set

for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ) holds

EnsCat E is with_coproducts

for A being ObjectsFamily of I,(EnsCat E) holds Union (coprod A) in E ) holds

EnsCat E is with_coproducts

proof end;