let X be set ; :: thesis: CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X),(CId X) #) is Category
set M = MapsC X;
set d = CDom X;
set c = CCod X;
set p = CComp X;
set i = CId X;

now

thus for f, g being Element of MapsC X holds
( [g,f] in dom (CComp X) iff (CDom X) . g = (CCod X) . f ) :: thesis: ( ( for f, g being Element of MapsC X st (CDom X) . g = (CCod X) . f holds
( (CDom X) . ((CComp X) . (g,f)) = (CDom X) . f & (CCod X) . ((CComp X) . (g,f)) = (CCod X) . g ) ) & ( for f, g, h being Element of MapsC X st (CDom X) . h = (CCod X) . g & (CDom X) . g = (CCod X) . f holds
(CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . (((CComp X) . (h,g)),f) ) & ( for b being Element of CSp X holds
( (CDom X) . ((CId X) . b) = b & (CCod X) . ((CId X) . b) = b & ( for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f ) & ( for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g ) ) ) )

proof

let f, g be Element of MapsC X; :: thesis: ( [g,f] in dom (CComp X) iff (CDom X) . g = (CCod X) . f )
( (CDom X) . g = dom g & (CCod X) . f = cod f ) by Def14, Def15;
hence ( [g,f] in dom (CComp X) iff (CDom X) . g = (CCod X) . f ) by Def16; :: thesis: verum

end;

thus for f, g being Element of MapsC X st (CDom X) . g = (CCod X) . f holds
( (CDom X) . ((CComp X) . (g,f)) = (CDom X) . f & (CCod X) . ((CComp X) . (g,f)) = (CCod X) . g ) :: thesis: ( ( for f, g, h being Element of MapsC X st (CDom X) . h = (CCod X) . g & (CDom X) . g = (CCod X) . f holds
(CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . (((CComp X) . (h,g)),f) ) & ( for b being Element of CSp X holds
( (CDom X) . ((CId X) . b) = b & (CCod X) . ((CId X) . b) = b & ( for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f ) & ( for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g ) ) ) )

proof

let f, g be Element of MapsC X; :: thesis: ( (CDom X) . g = (CCod X) . f implies ( (CDom X) . ((CComp X) . (g,f)) = (CDom X) . f & (CCod X) . ((CComp X) . (g,f)) = (CCod X) . g ) )
assume A1: (CDom X) . g = (CCod X) . f ; :: thesis: ( (CDom X) . ((CComp X) . (g,f)) = (CDom X) . f & (CCod X) . ((CComp X) . (g,f)) = (CCod X) . g )
A2: ( (CDom X) . g = dom g & (CCod X) . f = cod f ) by Def14, Def15;
then A3: (CComp X) . [g,f] = g * f by A1, Def16;
A4: ( (CDom X) . f = dom f & (CCod X) . g = cod g ) by Def14, Def15;
( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th22;
hence ( (CDom X) . ((CComp X) . (g,f)) = (CDom X) . f & (CCod X) . ((CComp X) . (g,f)) = (CCod X) . g ) by A3, A4, Def14, Def15; :: thesis: verum

end;

thus for f, g, h being Element of MapsC X st (CDom X) . h = (CCod X) . g & (CDom X) . g = (CCod X) . f holds
(CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . (((CComp X) . (h,g)),f) :: thesis: for b being Element of CSp X holds
( (CDom X) . ((CId X) . b) = b & (CCod X) . ((CId X) . b) = b & ( for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f ) & ( for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g ) )

proof

let f, g, h be Element of MapsC X; :: thesis: ( (CDom X) . h = (CCod X) . g & (CDom X) . g = (CCod X) . f implies (CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . (((CComp X) . (h,g)),f) )
assume that
A5: (CDom X) . h = (CCod X) . g and
A6: (CDom X) . g = (CCod X) . f ; :: thesis: (CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . (((CComp X) . (h,g)),f)
A7: ( dom h = (CDom X) . h & cod g = (CCod X) . g ) by Def14, Def15;
then A8: dom (h * g) = dom g by A5, Th22;
A9: ( dom g = (CDom X) . g & cod f = (CCod X) . f ) by Def14, Def15;
then A10: cod (g * f) = dom h by A5, A6, A7, Th22;
thus (CComp X) . (h,((CComp X) . (g,f))) = (CComp X) . [h,(g * f)] by A6, A9, Def16
.= h * (g * f) by A10, Def16
.= (h * g) * f by A5, A6, A7, A9, Th23
.= (CComp X) . [(h * g),f] by A6, A9, A8, Def16
.= (CComp X) . (((CComp X) . (h,g)),f) by A5, A7, Def16 ; :: thesis: verum

end;

let b be Element of CSp X; :: thesis: ( (CDom X) . ((CId X) . b) = b & (CCod X) . ((CId X) . b) = b & ( for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f ) & ( for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g ) )
A11: (CId X) . b = id$ b by Def17;
A12: cod (id$ b) = b by Th24;
A13: dom (id$ b) = b by Th24;
hence ( (CDom X) . ((CId X) . b) = b & (CCod X) . ((CId X) . b) = b ) by A11, A12, Def14, Def15; :: thesis: ( ( for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f ) & ( for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g ) )
thus for f being Element of MapsC X st (CCod X) . f = b holds
(CComp X) . (((CId X) . b),f) = f :: thesis: for g being Element of MapsC X st (CDom X) . g = b holds
(CComp X) . (g,((CId X) . b)) = g

proof

let f be Element of MapsC X; :: thesis: ( (CCod X) . f = b implies (CComp X) . (((CId X) . b),f) = f )
assume A14: (CCod X) . f = b ; :: thesis: (CComp X) . (((CId X) . b),f) = f
A15: cod f = (CCod X) . f by Def15;
then (id$ b) * f = f by A14, Th25;
hence (CComp X) . (((CId X) . b),f) = f by A11, A13, A14, A15, Def16; :: thesis: verum

end;

let g be Element of MapsC X; :: thesis: ( (CDom X) . g = b implies (CComp X) . (g,((CId X) . b)) = g )
assume A16: (CDom X) . g = b ; :: thesis: (CComp X) . (g,((CId X) . b)) = g
A17: dom g = (CDom X) . g by Def14;
then g * (id$ b) = g by A16, Th25;
hence (CComp X) . (g,((CId X) . b)) = g by A11, A12, A16, A17, Def16; :: thesis: verum

end;

hence CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X),(CId X) #) is Category by CAT_1:def 5; :: thesis: verum