let o, m be set ; :: thesis: c1Cat* o,m is Category-like
set C = c1Cat* o,m;
set CP = the Comp of (c1Cat* o,m);
set CD = the Source of (c1Cat* o,m);
set CC = the Target of (c1Cat* o,m);
set CI = the Id of (c1Cat* o,m);
thus for f, g being Morphism of (c1Cat* o,m) holds
( [g,f] in dom the Comp of (c1Cat* o,m) iff the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f ) :: according to CAT_1:def 8 :: thesis: ( ( for b1, b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b2 = the Target of (c1Cat* o,m) . b1 or ( the Source of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . b2,b1) = the Source of (c1Cat* o,m) . b1 & the Target of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . b2,b1) = the Target of (c1Cat* o,m) . b2 ) ) ) & ( for b1, b2, b3 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b3 = the Target of (c1Cat* o,m) . b2 or not the Source of (c1Cat* o,m) . b2 = the Target of (c1Cat* o,m) . b1 or the Comp of (c1Cat* o,m) . b3,(the Comp of (c1Cat* o,m) . b2,b1) = the Comp of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of (c1Cat* o,m) holds
( the Source of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & the Target of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Target of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . b2,(the Id of (c1Cat* o,m) . b1) = b2 ) ) ) ) )
proof
let f, g be Morphism of (c1Cat* o,m); :: thesis: ( [g,f] in dom the Comp of (c1Cat* o,m) iff the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f )
A1: dom the Comp of (c1Cat* o,m) = {[m,m]} by FUNCOP_1:19;
( f = m & g = m ) by TARSKI:def 1;
hence ( [g,f] in dom the Comp of (c1Cat* o,m) iff the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f ) by A1, TARSKI:def 1; :: thesis: verum
end;
thus for f, g being Morphism of (c1Cat* o,m) st the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f holds
( the Source of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Source of (c1Cat* o,m) . f & the Target of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Target of (c1Cat* o,m) . g ) :: thesis: ( ( for b1, b2, b3 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b3 = the Target of (c1Cat* o,m) . b2 or not the Source of (c1Cat* o,m) . b2 = the Target of (c1Cat* o,m) . b1 or the Comp of (c1Cat* o,m) . b3,(the Comp of (c1Cat* o,m) . b2,b1) = the Comp of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . b3,b2),b1 ) ) & ( for b1 being Element of the carrier of (c1Cat* o,m) holds
( the Source of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & the Target of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Target of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . b2,(the Id of (c1Cat* o,m) . b1) = b2 ) ) ) ) )
proof
let f, g be Morphism of (c1Cat* o,m); :: thesis: ( the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f implies ( the Source of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Source of (c1Cat* o,m) . f & the Target of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Target of (c1Cat* o,m) . g ) )
the Comp of (c1Cat* o,m) . g,f = m by FUNCOP_1:92;
then reconsider gf = the Comp of (c1Cat* o,m) . g,f as Morphism of (c1Cat* o,m) by TARSKI:def 1;
the Source of (c1Cat* o,m) . gf = o by FUNCT_2:65;
hence ( the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f implies ( the Source of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Source of (c1Cat* o,m) . f & the Target of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . g,f) = the Target of (c1Cat* o,m) . g ) ) by FUNCT_2:65; :: thesis: verum
end;
thus for f, g, h being Morphism of (c1Cat* o,m) st the Source of (c1Cat* o,m) . h = the Target of (c1Cat* o,m) . g & the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f holds
the Comp of (c1Cat* o,m) . h,(the Comp of (c1Cat* o,m) . g,f) = the Comp of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . h,g),f :: thesis: for b1 being Element of the carrier of (c1Cat* o,m) holds
( the Source of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & the Target of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1) = b1 & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Target of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b1),b2 = b2 ) ) & ( for b2 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b2 = b1 or the Comp of (c1Cat* o,m) . b2,(the Id of (c1Cat* o,m) . b1) = b2 ) ) )
proof
let f, g, h be Morphism of (c1Cat* o,m); :: thesis: ( the Source of (c1Cat* o,m) . h = the Target of (c1Cat* o,m) . g & the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f implies the Comp of (c1Cat* o,m) . h,(the Comp of (c1Cat* o,m) . g,f) = the Comp of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . h,g),f )
( the Comp of (c1Cat* o,m) . g,f = m & the Comp of (c1Cat* o,m) . h,g = m ) by FUNCOP_1:92;
then reconsider gf = the Comp of (c1Cat* o,m) . g,f, hg = the Comp of (c1Cat* o,m) . h,g as Morphism of (c1Cat* o,m) by TARSKI:def 1;
( the Comp of (c1Cat* o,m) . h,gf = m & the Comp of (c1Cat* o,m) . hg,f = m ) by FUNCOP_1:92;
hence ( the Source of (c1Cat* o,m) . h = the Target of (c1Cat* o,m) . g & the Source of (c1Cat* o,m) . g = the Target of (c1Cat* o,m) . f implies the Comp of (c1Cat* o,m) . h,(the Comp of (c1Cat* o,m) . g,f) = the Comp of (c1Cat* o,m) . (the Comp of (c1Cat* o,m) . h,g),f ) ; :: thesis: verum
end;
let b be Object of (c1Cat* o,m); :: thesis: ( the Source of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b) = b & the Target of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b) = b & ( for b1 being Element of the carrier' of (c1Cat* o,m) holds
( not the Target of (c1Cat* o,m) . b1 = b or the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b1 = b or the Comp of (c1Cat* o,m) . b1,(the Id of (c1Cat* o,m) . b) = b1 ) ) )
b = o by TARSKI:def 1;
hence ( the Source of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b) = b & the Target of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b) = b ) by FUNCT_2:65; :: thesis: ( ( for b1 being Element of the carrier' of (c1Cat* o,m) holds
( not the Target of (c1Cat* o,m) . b1 = b or the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b),b1 = b1 ) ) & ( for b1 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b1 = b or the Comp of (c1Cat* o,m) . b1,(the Id of (c1Cat* o,m) . b) = b1 ) ) )
thus for f being Morphism of (c1Cat* o,m) st the Target of (c1Cat* o,m) . f = b holds
the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b),f = f :: thesis: for b1 being Element of the carrier' of (c1Cat* o,m) holds
( not the Source of (c1Cat* o,m) . b1 = b or the Comp of (c1Cat* o,m) . b1,(the Id of (c1Cat* o,m) . b) = b1 )
proof
let f be Morphism of (c1Cat* o,m); :: thesis: ( the Target of (c1Cat* o,m) . f = b implies the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b),f = f )
f = m by TARSKI:def 1;
hence ( the Target of (c1Cat* o,m) . f = b implies the Comp of (c1Cat* o,m) . (the Id of (c1Cat* o,m) . b),f = f ) by FUNCOP_1:92; :: thesis: verum
end;
let g be Morphism of (c1Cat* o,m); :: thesis: ( not the Source of (c1Cat* o,m) . g = b or the Comp of (c1Cat* o,m) . g,(the Id of (c1Cat* o,m) . b) = g )
assume the Source of (c1Cat* o,m) . g = b ; :: thesis: the Comp of (c1Cat* o,m) . g,(the Id of (c1Cat* o,m) . b) = g
g = m by TARSKI:def 1;
hence the Comp of (c1Cat* o,m) . g,(the Id of (c1Cat* o,m) . b) = g by FUNCOP_1:92; :: thesis: verum