let A be Category; :: thesis: for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let O be non empty Subset of the carrier of A; :: thesis: for M being non empty Subset of the carrier' of A
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let M be non empty Subset of the carrier' of A; :: thesis: for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let DOM, COD be Function of M,O; :: thesis: ( DOM = the Source of A | M & COD = the Target of A | M implies for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume that
A1: DOM = the Source of A | M and
A2: COD = the Target of A | M ; :: thesis: for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let COMP be PartFunc of [:M,M:],M; :: thesis: ( COMP = the Comp of A || M implies for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume A3: COMP = the Comp of A || M ; :: thesis: for ID being Function of O,M st ID = the Id of A | O holds
CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
let ID be Function of O,M; :: thesis: ( ID = the Id of A | O implies CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A )
assume A4: ID = the Id of A | O ; :: thesis: CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A
set C = CatStr(# O,M,DOM,COD,COMP,ID #);
A5: now
let f be Morphism of A; :: thesis: for g being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) st f = g holds
( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )
let g be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( f = g implies ( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g ) )
assume A6: f = g ; :: thesis: ( the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )
dom the Source of CatStr(# O,M,DOM,COD,COMP,ID #) = the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) by FUNCT_2:def 1;
hence the Source of A . f = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g by A1, A6, FUNCT_1:70; :: thesis: the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g
dom the Target of CatStr(# O,M,DOM,COD,COMP,ID #) = the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) by FUNCT_2:def 1;
hence the Target of A . f = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g by A2, A6, FUNCT_1:70; :: thesis: verum
end;
A7: dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) = (dom the Comp of A) /\ [:the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #),the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #):] by A3, RELAT_1:90;
A8: now
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
assume the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f ; :: thesis: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #)
then the Source of A . g9 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5
.= the Target of A . f9 by A5 ;
then A9: [g9,f9] in dom the Comp of A by CAT_1:def 8;
[g,f] in [:the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #),the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #):] by ZFMISC_1:106;
hence [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) by A7, A9, XBOOLE_0:def 4; :: thesis: verum
end;
A10: dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) c= dom the Comp of A by A3, RELAT_1:89;
CatStr(# O,M,DOM,COD,COMP,ID #) is Category-like
proof
thus for f, g being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) iff the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f ) :: according to CAT_1:def 8 :: thesis: ( ( for b1, b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 ) ) ) & ( for b1, b2, b3 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b3 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 or not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) ) ) )
proof
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) iff the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
thus ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) implies the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f ) :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) )
proof
assume A11: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) ; :: thesis: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f
thus the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Source of A . g9 by A5
.= the Target of A . f9 by A10, A11, CAT_1:def 8
.= the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5 ; :: thesis: verum
end;
thus ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) ) by A8; :: thesis: verum
end;
thus for f, g being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) st the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g ) :: thesis: ( ( for b1, b2, b3 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b3 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 or not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,b1) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) ) ) )
proof
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g ) )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
assume A12: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f ; :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g )
then A13: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [g,f] is Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) by A8, PARTFUN1:27;
A14: the Source of A . g9 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5, A12
.= the Target of A . f9 by A5 ;
A15: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [g,f] = the Comp of A . [g9,f9] by A3, A8, A12, FUNCT_1:70;
then A16: the Comp of A . [g9,f9] is Morphism of A by A13, TARSKI:def 3;
hence the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Source of A . (the Comp of A . g9,f9) by A5, A15, A13
.= the Source of A . f9 by A14, CAT_1:def 8
.= the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5 ;
:: thesis: the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g
thus the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Target of A . (the Comp of A . g9,f9) by A5, A15, A13, A16
.= the Target of A . g9 by A14, CAT_1:def 8
.= the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g by A5 ; :: thesis: verum
end;
thus for f, g, h being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) st the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . h = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f holds
the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f :: thesis: for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b1 & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b2 = b1 or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b2,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b1) = b2 ) ) )
proof
let f, g, h be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . h = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g & the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f implies the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f )
reconsider g9 = g, f9 = f, h9 = h as Morphism of A by TARSKI:def 3;
assume that
A17: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . h = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g and
A18: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f ; :: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f
reconsider gf = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [g,f], hg = the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [h,g] as Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) by A8, A17, A18, PARTFUN1:27;
A19: the Source of A . h9 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . g by A5, A17
.= the Target of A . g9 by A5 ;
then A20: [h9,g9] in dom the Comp of A by CAT_1:def 8;
A21: the Source of A . g9 = the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5, A18
.= the Target of A . f9 by A5 ;
then [g9,f9] in dom the Comp of A by CAT_1:def 8;
then reconsider gf9 = the Comp of A . g9,f9, hg9 = the Comp of A . h9,g9 as Morphism of A by A20, PARTFUN1:27;
A22: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [h,g] = the Comp of A . [h9,g9] by A3, A8, A17, FUNCT_1:70;
then A23: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . hg = the Source of A . hg9 by A5
.= the Source of A . g9 by A19, CAT_1:def 8
.= the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f by A5, A18 ;
A24: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . [g,f] = the Comp of A . [g9,f9] by A3, A8, A18, FUNCT_1:70;
the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . h = the Target of A . g9 by A5, A17
.= the Target of A . gf9 by A21, CAT_1:def 8
.= the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . gf by A5, A24 ;
hence the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,(the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,f) = the Comp of A . h9,(the Comp of A . g9,f9) by A3, A8, A24, FUNCT_1:70
.= the Comp of A . (the Comp of A . h9,g9),f9 by A19, A21, CAT_1:def 8
.= the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . h,g),f by A3, A8, A22, A23, FUNCT_1:70 ;
:: thesis: verum
end;
let b be Object of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
reconsider b9 = b as Object of A by TARSKI:def 3;
dom the Id of CatStr(# O,M,DOM,COD,COMP,ID #) = the carrier of CatStr(# O,M,DOM,COD,COMP,ID #) by FUNCT_2:def 1;
then A25: the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b = the Id of A . b9 by A4, FUNCT_1:70;
hence the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = the Source of A . (the Id of A . b9) by A5
.= b by CAT_1:def 8 ;
:: thesis: ( the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
thus the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = the Target of A . (the Id of A . b9) by A5, A25
.= b by CAT_1:def 8 ; :: thesis: ( ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 ) ) )
thus for f being Morphism of CatStr(# O,M,DOM,COD,COMP,ID #) st the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f = b holds
the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = f :: thesis: for b1 being Element of the carrier' of CatStr(# O,M,DOM,COD,COMP,ID #) holds
( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . b1 = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . b1,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = b1 )
proof
let f be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f = b implies the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = f )
assume A26: the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f = b ; :: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = f
reconsider f9 = f as Morphism of A by TARSKI:def 3;
A27: the Target of A . f9 = b9 by A5, A26;
the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . f = the Target of A . f9 by A5
.= the Source of A . (the Id of A . b9) by A27, CAT_1:def 8
.= the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) by A5, A25 ;
hence the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b),f = the Comp of A . (the Id of A . b9),f9 by A3, A8, A25, FUNCT_1:70
.= f by A27, CAT_1:def 8 ;
:: thesis: verum
end;
let g be Morphism of CatStr(# O,M,DOM,COD,COMP,ID #); :: thesis: ( not the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = b or the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = g )
assume A28: the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = b ; :: thesis: the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = g
reconsider g9 = g as Morphism of A by TARSKI:def 3;
A29: the Source of A . g9 = b9 by A5, A28;
the Source of CatStr(# O,M,DOM,COD,COMP,ID #) . g = the Source of A . g9 by A5
.= the Target of A . (the Id of A . b9) by A29, CAT_1:def 8
.= the Target of CatStr(# O,M,DOM,COD,COMP,ID #) . (the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) by A5, A25 ;
hence the Comp of CatStr(# O,M,DOM,COD,COMP,ID #) . g,(the Id of CatStr(# O,M,DOM,COD,COMP,ID #) . b) = the Comp of A . g9,(the Id of A . b9) by A3, A8, A25, FUNCT_1:70
.= g by A29, CAT_1:def 8 ;
:: thesis: verum
end;
then reconsider C = CatStr(# O,M,DOM,COD,COMP,ID #) as Category ;
C is Subcategory of A
proof
thus the carrier of C c= the carrier of A ; :: according to CAT_2:def 4 :: thesis: ( ( for b1, b2 being Element of the carrier of C
for b3, b4 being Element of the carrier of A holds
( not b1 = b3 or not b2 = b4 or Hom b1,b2 c= Hom b3,b4 ) ) & the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus for a, b being Object of C
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 :: thesis: ( the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
proof
let a, b be Object of C; :: thesis: for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9
let a9, b9 be Object of A; :: thesis: ( a = a9 & b = b9 implies Hom a,b c= Hom a9,b9 )
assume that
A30: a = a9 and
A31: b = b9 ; :: thesis: Hom a,b c= Hom a9,b9
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom a,b or x in Hom a9,b9 )
assume x in Hom a,b ; :: thesis: x in Hom a9,b9
then consider f being Morphism of C such that
A32: x = f and
A33: dom f = a and
A34: cod f = b ;
reconsider f9 = f as Morphism of A by TARSKI:def 3;
A35: cod f9 = b9 by A5, A31, A34;
dom f9 = a9 by A5, A30, A33;
hence x in Hom a9,b9 by A32, A35; :: thesis: verum
end;
A36: dom the Id of C = the carrier of C by FUNCT_2:def 1;
thus the Comp of C c= the Comp of A by A3, RELAT_1:88; :: thesis: for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of C; :: thesis: for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )
let a9 be Object of A; :: thesis: ( not a = a9 or id a = id a9 )
assume a = a9 ; :: thesis: id a = id a9
hence id a = id a9 by A4, A36, FUNCT_1:70; :: thesis: verum
end;
hence CatStr(# O,M,DOM,COD,COMP,ID #) is Subcategory of A ; :: thesis: verum