environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, CLASSES1, ZFMISC_1, EQREL_1, TOLER_1, SETFAM_1, SUBSET_1, FUNCT_2, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, ENS_1, PARTFUN1, CAT_1, COH_SP, STRUCT_0, MONOID_0, RELAT_2, BINOP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, MCART_1, FUNCT_1, PARTFUN1, CLASSES1, FUNCT_2, BINOP_1, EQREL_1, TOLER_1, STRUCT_0, GRAPH_1, CAT_1;
definitions TARSKI, CLASSES1, XBOOLE_0, RELAT_1, CAT_1;
theorems TARSKI, ZFMISC_1, TOLER_1, ENUMSET1, RELAT_1, FUNCT_2, CLASSES1, PARTFUN1, FUNCT_1, DOMAIN_1, CAT_1, XBOOLE_0, XBOOLE_1, EQREL_1, XTUPLE_0;
schemes TOLER_1, TARSKI, FUNCT_2, BINOP_1, XBOOLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, EQREL_1, CAT_2, CAT_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, EQREL_1, CLASSES1, TOLER_1, CAT_1, RELSET_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, CAT_1, GRAPH_1;
expansions TARSKI, RELAT_1, CAT_1;
Lm1:
for X being set
for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1
Lm2:
for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )
definition
let X be
set ;
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = dom l
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) & ( for l being Element of MapsC X holds b2 . l = dom l ) holds
b1 = b2
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = cod l
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) & ( for l being Element of MapsC X holds b2 . l = cod l ) holds
b1 = b2
existence
ex b1 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) )
uniqueness
for b1, b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) holds
b1 = b2
end;
Lm3:
for X being set
for a being Element of (CohCat X)
for aa being Element of CSp X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
for b being Element of (CohCat X) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
Lm4:
for X being set
for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1
definition
let X be
set ;
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = dom m
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) & ( for m being Element of MapsT X holds b2 . m = dom m ) holds
b1 = b2
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = cod m
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) & ( for m being Element of MapsT X holds b2 . m = cod m ) holds
b1 = b2
existence
ex b1 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
uniqueness
for b1, b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
end;
Lm5:
for X being set
for a being Element of (TolCat X)
for aa being Element of TOL X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
for b being Element of (TolCat X) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )