let X be set ; :: thesis: CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X),(fId X) #) is Category
set M = MapsT X;
set d = fDom X;
set c = fCod X;
set p = fComp X;
set i = fId X;

now

thus for f, g being Element of MapsT X holds
( [g,f] in dom (fComp X) iff (fDom X) . g = (fCod X) . f ) :: thesis: ( ( for f, g being Element of MapsT X st (fDom X) . g = (fCod X) . f holds
( (fDom X) . ((fComp X) . (g,f)) = (fDom X) . f & (fCod X) . ((fComp X) . (g,f)) = (fCod X) . g ) ) & ( for f, g, h being Element of MapsT X st (fDom X) . h = (fCod X) . g & (fDom X) . g = (fCod X) . f holds
(fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . (((fComp X) . (h,g)),f) ) & ( for b being Element of TOL X holds
( (fDom X) . ((fId X) . b) = b & (fCod X) . ((fId X) . b) = b & ( for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f ) & ( for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g ) ) ) )

proof

let f, g be Element of MapsT X; :: thesis: ( [g,f] in dom (fComp X) iff (fDom X) . g = (fCod X) . f )
( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def29, Def30;
hence ( [g,f] in dom (fComp X) iff (fDom X) . g = (fCod X) . f ) by Def31; :: thesis: verum

end;

thus for f, g being Element of MapsT X st (fDom X) . g = (fCod X) . f holds
( (fDom X) . ((fComp X) . (g,f)) = (fDom X) . f & (fCod X) . ((fComp X) . (g,f)) = (fCod X) . g ) :: thesis: ( ( for f, g, h being Element of MapsT X st (fDom X) . h = (fCod X) . g & (fDom X) . g = (fCod X) . f holds
(fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . (((fComp X) . (h,g)),f) ) & ( for b being Element of TOL X holds
( (fDom X) . ((fId X) . b) = b & (fCod X) . ((fId X) . b) = b & ( for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f ) & ( for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g ) ) ) )

proof

let f, g be Element of MapsT X; :: thesis: ( (fDom X) . g = (fCod X) . f implies ( (fDom X) . ((fComp X) . (g,f)) = (fDom X) . f & (fCod X) . ((fComp X) . (g,f)) = (fCod X) . g ) )
assume A1: (fDom X) . g = (fCod X) . f ; :: thesis: ( (fDom X) . ((fComp X) . (g,f)) = (fDom X) . f & (fCod X) . ((fComp X) . (g,f)) = (fCod X) . g )
A2: ( (fDom X) . g = dom g & (fCod X) . f = cod f ) by Def29, Def30;
then A3: (fComp X) . [g,f] = g * f by A1, Def31;
A4: ( (fDom X) . f = dom f & (fCod X) . g = cod g ) by Def29, Def30;
( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th45;
hence ( (fDom X) . ((fComp X) . (g,f)) = (fDom X) . f & (fCod X) . ((fComp X) . (g,f)) = (fCod X) . g ) by A3, A4, Def29, Def30; :: thesis: verum

end;

thus for f, g, h being Element of MapsT X st (fDom X) . h = (fCod X) . g & (fDom X) . g = (fCod X) . f holds
(fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . (((fComp X) . (h,g)),f) :: thesis: for b being Element of TOL X holds
( (fDom X) . ((fId X) . b) = b & (fCod X) . ((fId X) . b) = b & ( for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f ) & ( for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g ) )

proof

let f, g, h be Element of MapsT X; :: thesis: ( (fDom X) . h = (fCod X) . g & (fDom X) . g = (fCod X) . f implies (fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . (((fComp X) . (h,g)),f) )
assume that
A5: (fDom X) . h = (fCod X) . g and
A6: (fDom X) . g = (fCod X) . f ; :: thesis: (fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . (((fComp X) . (h,g)),f)
A7: ( dom h = (fDom X) . h & cod g = (fCod X) . g ) by Def29, Def30;
then A8: dom (h * g) = dom g by A5, Th45;
A9: ( dom g = (fDom X) . g & cod f = (fCod X) . f ) by Def29, Def30;
then A10: cod (g * f) = dom h by A5, A6, A7, Th45;
thus (fComp X) . (h,((fComp X) . (g,f))) = (fComp X) . [h,(g * f)] by A6, A9, Def31
.= h * (g * f) by A10, Def31
.= (h * g) * f by A5, A6, A7, A9, Th46
.= (fComp X) . [(h * g),f] by A6, A9, A8, Def31
.= (fComp X) . (((fComp X) . (h,g)),f) by A5, A7, Def31 ; :: thesis: verum

end;

let b be Element of TOL X; :: thesis: ( (fDom X) . ((fId X) . b) = b & (fCod X) . ((fId X) . b) = b & ( for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f ) & ( for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g ) )
A11: (fId X) . b = id$ b by Def32;
A12: cod (id$ b) = b by Th47;
A13: dom (id$ b) = b by Th47;
hence ( (fDom X) . ((fId X) . b) = b & (fCod X) . ((fId X) . b) = b ) by A11, A12, Def29, Def30; :: thesis: ( ( for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f ) & ( for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g ) )
thus for f being Element of MapsT X st (fCod X) . f = b holds
(fComp X) . (((fId X) . b),f) = f :: thesis: for g being Element of MapsT X st (fDom X) . g = b holds
(fComp X) . (g,((fId X) . b)) = g

proof

let f be Element of MapsT X; :: thesis: ( (fCod X) . f = b implies (fComp X) . (((fId X) . b),f) = f )
assume A14: (fCod X) . f = b ; :: thesis: (fComp X) . (((fId X) . b),f) = f
A15: cod f = (fCod X) . f by Def30;
then (id$ b) * f = f by A14, Th48;
hence (fComp X) . (((fId X) . b),f) = f by A11, A13, A14, A15, Def31; :: thesis: verum

end;

let g be Element of MapsT X; :: thesis: ( (fDom X) . g = b implies (fComp X) . (g,((fId X) . b)) = g )
assume A16: (fDom X) . g = b ; :: thesis: (fComp X) . (g,((fId X) . b)) = g
A17: dom g = (fDom X) . g by Def29;
then g * (id$ b) = g by A16, Th48;
hence (fComp X) . (g,((fId X) . b)) = g by A11, A12, A16, A17, Def31; :: thesis: verum

end;

hence CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X),(fId X) #) is Category by CAT_1:def 5; :: thesis: verum