let V be non empty set ; :: thesis: CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is Category
set M = Maps V;
set d = fDom V;
set c = fCod V;
set p = fComp V;
set i = fId V;

now

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

proof

let f, g be Element of Maps V; :: thesis: ( [g,f] in dom (fComp V) iff (fDom V) . g = (fCod V) . f )
( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def10, Def11;
hence ( [g,f] in dom (fComp V) iff (fDom V) . g = (fCod V) . f ) by Def12; :: thesis: verum

end;

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

proof

let f, g be Element of Maps V; :: thesis: ( (fDom V) . g = (fCod V) . f implies ( (fDom V) . ((fComp V) . (g,f)) = (fDom V) . f & (fCod V) . ((fComp V) . (g,f)) = (fCod V) . g ) )
assume A1: (fDom V) . g = (fCod V) . f ; :: thesis: ( (fDom V) . ((fComp V) . (g,f)) = (fDom V) . f & (fCod V) . ((fComp V) . (g,f)) = (fCod V) . g )
A2: ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def10, Def11;
then A3: (fComp V) . [g,f] = g * f by A1, Def12;
A4: ( (fDom V) . f = dom f & (fCod V) . g = cod g ) by Def10, Def11;
( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, A2, Th12;
hence ( (fDom V) . ((fComp V) . (g,f)) = (fDom V) . f & (fCod V) . ((fComp V) . (g,f)) = (fCod V) . g ) by A3, A4, Def10, Def11; :: thesis: verum

end;

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

proof

let f, g, h be Element of Maps V; :: thesis: ( (fDom V) . h = (fCod V) . g & (fDom V) . g = (fCod V) . f implies (fComp V) . (h,((fComp V) . (g,f))) = (fComp V) . (((fComp V) . (h,g)),f) )
assume that
A5: (fDom V) . h = (fCod V) . g and
A6: (fDom V) . g = (fCod V) . f ; :: thesis: (fComp V) . (h,((fComp V) . (g,f))) = (fComp V) . (((fComp V) . (h,g)),f)
A7: ( dom h = (fDom V) . h & cod g = (fCod V) . g ) by Def10, Def11;
then A8: dom (h * g) = dom g by A5, Th12;
A9: ( dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def10, Def11;
then A10: cod (g * f) = dom h by A5, A6, A7, Th12;
thus (fComp V) . (h,((fComp V) . (g,f))) = (fComp V) . [h,(g * f)] by A6, A9, Def12
.= h * (g * f) by A10, Def12
.= (h * g) * f by A5, A6, A7, A9, Th13
.= (fComp V) . [(h * g),f] by A6, A9, A8, Def12
.= (fComp V) . (((fComp V) . (h,g)),f) by A5, A7, Def12 ; :: thesis: verum

end;

let b be Element of V; :: thesis: ( (fDom V) . ((fId V) . b) = b & (fCod V) . ((fId V) . b) = b & ( for f being Element of Maps V st (fCod V) . f = b holds
(fComp V) . (((fId V) . b),f) = f ) & ( for g being Element of Maps V st (fDom V) . g = b holds
(fComp V) . (g,((fId V) . b)) = g ) )
A11: (fId V) . b = id$ b by Def13;
A12: cod (id$ b) = b by Th11;
A13: dom (id$ b) = b by Th11;
hence ( (fDom V) . ((fId V) . b) = b & (fCod V) . ((fId V) . b) = b ) by A11, A12, Def10, Def11; :: thesis: ( ( for f being Element of Maps V st (fCod V) . f = b holds
(fComp V) . (((fId V) . b),f) = f ) & ( for g being Element of Maps V st (fDom V) . g = b holds
(fComp V) . (g,((fId V) . b)) = g ) )
thus for f being Element of Maps V st (fCod V) . f = b holds
(fComp V) . (((fId V) . b),f) = f :: thesis: for g being Element of Maps V st (fDom V) . g = b holds
(fComp V) . (g,((fId V) . b)) = g

proof

let f be Element of Maps V; :: thesis: ( (fCod V) . f = b implies (fComp V) . (((fId V) . b),f) = f )
assume A14: (fCod V) . f = b ; :: thesis: (fComp V) . (((fId V) . b),f) = f
A15: cod f = (fCod V) . f by Def11;
then (id$ b) * f = f by A14, Th14;
hence (fComp V) . (((fId V) . b),f) = f by A11, A13, A14, A15, Def12; :: thesis: verum

end;

let g be Element of Maps V; :: thesis: ( (fDom V) . g = b implies (fComp V) . (g,((fId V) . b)) = g )
assume A16: (fDom V) . g = b ; :: thesis: (fComp V) . (g,((fId V) . b)) = g
A17: dom g = (fDom V) . g by Def10;
then g * (id$ b) = g by A16, Th14;
hence (fComp V) . (g,((fId V) . b)) = g by A11, A12, A16, A17, Def12; :: thesis: verum

end;

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