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 )
( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def10, Def11;
then ( dom (g * f) = dom f & cod (g * f) = cod g & (fComp V) . [g,f] = g * f & (fDom V) . f = dom f & (fCod V) . g = cod g ) by A1, Def10, Def11, Def12, Th12;
hence ( (fDom V) . ((fComp V) . g,f) = (fDom V) . f & (fCod V) . ((fComp V) . g,f) = (fCod V) . g ) by 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
A2: (fDom V) . h = (fCod V) . g and
A3: (fDom V) . g = (fCod V) . f ; :: thesis: (fComp V) . h,((fComp V) . g,f) = (fComp V) . ((fComp V) . h,g),f
A4: ( dom h = (fDom V) . h & cod g = (fCod V) . g & dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def10, Def11;
then A5: ( cod (g * f) = dom h & dom (h * g) = dom g ) by A2, A3, Th12;
thus (fComp V) . h,((fComp V) . g,f) = (fComp V) . [h,(g * f)] by A3, A4, Def12
.= h * (g * f) by A5, Def12
.= (h * g) * f by A2, A3, A4, Th13
.= (fComp V) . [(h * g),f] by A3, A4, A5, Def12
.= (fComp V) . ((fComp V) . h,g),f by A2, A4, 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 ) )
A6: ( (fId V) . b = id$ b & dom (id$ b) = b & cod (id$ b) = b ) by Def13, Th11;
hence ( (fDom V) . ((fId V) . b) = b & (fCod V) . ((fId V) . b) = b ) by 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 A7: (fCod V) . f = b ; :: thesis: (fComp V) . ((fId V) . b),f = f
A8: cod f = (fCod V) . f by Def11;
then (id$ b) * f = f by A7, Th14;
hence (fComp V) . ((fId V) . b),f = f by A6, A7, A8, 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 A9: (fDom V) . g = b ; :: thesis: (fComp V) . g,((fId V) . b) = g
A10: dom g = (fDom V) . g by Def10;
then g * (id$ b) = g by A9, Th14;
hence (fComp V) . g,((fId V) . b) = g by A6, A9, A10, Def12; :: thesis: verum

end;

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