set M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } ;
set a0 = the Element of F1();
consider f0 being Element of F2() such that
A4: P1[ the Element of F1(), the Element of F1(),f0] and
for b being Element of F1()
for g being Element of F2() holds
( ( P1[ the Element of F1(),b,g] implies F3(g,f0) = g ) & ( P1[b, the Element of F1(),g] implies F3(f0,g) = g ) ) by A2;
A5: [[ the Element of F1(), the Element of F1()],f0] in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } by A4;
{ [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } c= [:[:F1(),F1():],F2():]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } or x in [:[:F1(),F1():],F2():] )
assume x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } ; :: thesis: x in [:[:F1(),F1():],F2():]
then ex a, b being Element of F1() ex f being Element of F2() st
( x = [[a,b],f] & P1[a,b,f] ) ;
hence x in [:[:F1(),F1():],F2():] ; :: thesis: verum
end;
then reconsider M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } as non empty Subset of [:[:F1(),F1():],F2():] by A5;
A6: now :: thesis: for m being Element of M holds
( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] )
let m be Element of M; :: thesis: ( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] )
m in M ;
then consider a, b being Element of F1(), f being Element of F2() such that
A7: m = [[a,b],f] and
A8: P1[a,b,f] ;
A9: m `11 = a by A7, MCART_1:85;
m `12 = b by A7, MCART_1:85;
hence ( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] ) by A7, A8, A9; :: thesis: verum
end;
deffunc H1( Element of M) -> Element of F1() = $1 `11 ;
consider DM being Function of M,F1() such that
A10: for m being Element of M holds DM . m = H1(m) from FUNCT_2:sch 4();
 deffunc H2( Element of M) -> Element of F1() = $1 `12 ;
consider CM being Function of M,F1() such that
A11: for m being Element of M holds CM . m = H2(m) from FUNCT_2:sch 4();
 deffunc H3( object , object ) -> object = [[($2 `11),($1 `12)],F3(($1 `2),($2 `2))];
defpred S1[ object , object ] means ( $1 `11 = $2 `12 & $1 in M & $2 in M );
A12: now :: thesis: for x, y being object st S1[x,y] holds
H3(x,y) in M
let x, y be object ; :: thesis: ( S1[x,y] implies H3(x,y) in M )
assume A13: S1[x,y] ; :: thesis: H3(x,y) in M
then consider ax, bx being Element of F1(), fx being Element of F2() such that
A14: x = [[ax,bx],fx] and
A15: P1[ax,bx,fx] ;
consider ay, b2 being Element of F1(), fy being Element of F2() such that
A16: y = [[ay,b2],fy] and
A17: P1[ay,b2,fy] by A13;
A18: x `11 = ax by A14, MCART_1:85;
A19: x `12 = bx by A14, MCART_1:85;
A20: y `11 = ay by A16, MCART_1:85;
A21: y `12 = b2 by A16, MCART_1:85;
A22: x `2 = fx by A14;
A23: y `2 = fy by A16;
A24: F3(fx,fy) in F2() by A1, A13, A15, A17, A18, A21;
P1[ay,bx,F3(fx,fy)] by A1, A13, A15, A17, A18, A21;
hence H3(x,y) in M by A19, A20, A22, A23, A24; :: thesis: verum
end;
consider CC being PartFunc of [:M,M:],M such that
A25: for x, y being object holds
( [x,y] in dom CC iff ( x in M & y in M & S1[x,y] ) ) and
A26: for x, y being object st [x,y] in dom CC holds
CC . (x,y) = H3(x,y) from BINOP_1:sch 6(A12);
 defpred S2[ Element of F1(), set ] means ex f being Element of F2() st
( $2 = [[$1,$1],f] & P1[$1,$1,f] & ( for b being Element of F1()
for g being Element of F2() holds
( ( P1[$1,b,g] implies F3(g,f) = g ) & ( P1[b,$1,g] implies F3(f,g) = g ) ) ) );
A27: now :: thesis: for a being Element of F1() ex y being Element of M st S2[a,y]
let a be Element of F1(); :: thesis: ex y being Element of M st S2[a,y]
consider f being Element of F2() such that
A28: P1[a,a,f] and
A29: for b being Element of F1()
for g being Element of F2() holds
( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) by A2;
[[a,a],f] in M by A28;
then reconsider y = [[a,a],f] as Element of M ;
take y = y; :: thesis: S2[a,y]
thus S2[a,y] by A28, A29; :: thesis: verum
end;
consider I being Function of F1(),M such that
A30: for o being Element of F1() holds S2[o,I . o] from FUNCT_2:sch 3(A27);
 set C = CatStr(# F1(),M,DM,CM,CC #);
A31: CatStr(# F1(),M,DM,CM,CC #) is Category-like
proof
hereby :: according to CAT_1:def 6 :: thesis: verum
let f, g be Morphism of CatStr(# F1(),M,DM,CM,CC #); :: thesis: ( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f )
A32: ( [g,f] in dom CC iff ( g in M & f in M & g `11 = f `12 & g in M & f in M ) ) by A25;
DM . g = g `11 by A10;
hence ( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f ) by A11, A32; :: thesis: verum
end;
end;
A33: for f, g being Morphism of CatStr(# F1(),M,DM,CM,CC #) holds
( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f ) by A31;
A34: CatStr(# F1(),M,DM,CM,CC #) is transitive
proof
let f, g be Morphism of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def 7 :: thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
A35: the Source of CatStr(# F1(),M,DM,CM,CC #) . f = f `11 by A10;
A36: the Source of CatStr(# F1(),M,DM,CM,CC #) . g = g `11 by A10;
A37: the Target of CatStr(# F1(),M,DM,CM,CC #) . f = f `12 by A11;
A38: the Target of CatStr(# F1(),M,DM,CM,CC #) . g = g `12 by A11;
assume A39: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A40: CC . (g,f) = [[(f `11),(g `12)],F3((g `2),(f `2))] by A26, A25, A36, A37;
A41: (CC . [g,f]) `11 = f `11 by A40, MCART_1:85;
A42: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f) = g (*) f by A39, A25, A36, A37, CAT_1:def 1;
(CC . [g,f]) `12 = g `12 by A40, MCART_1:85;
hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A10, A11, A35, A38, A41, A42; :: thesis: verum
end;
A43: CatStr(# F1(),M,DM,CM,CC #) is associative
proof
let f, g, h be Morphism of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def 8 :: thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
A44: the Source of CatStr(# F1(),M,DM,CM,CC #) . g = g `11 by A10;
A45: the Source of CatStr(# F1(),M,DM,CM,CC #) . h = h `11 by A10;
A46: the Target of CatStr(# F1(),M,DM,CM,CC #) . f = f `12 by A11;
A47: the Target of CatStr(# F1(),M,DM,CM,CC #) . g = g `12 by A11;
assume that
A48: dom h = cod g and
A49: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
A50: [g,f] in dom CC by A25, A44, A46, A49;
A51: [h,g] in dom CC by A25, A45, A47, A48;
A52: CC . [g,f] in rng CC by A50, FUNCT_1:def 3;
CC . [h,g] in rng CC by A51, FUNCT_1:def 3;
then reconsider gf = CC . (g,f), hg = CC . (h,g) as Element of M by A52;
A53: gf = [[(f `11),(g `12)],F3((g `2),(f `2))] by A26, A25, A44, A46, A49;
A54: hg = [[(g `11),(h `12)],F3((h `2),(g `2))] by A26, A25, A45, A47, A48;
A55: DM . gf = gf `11 by A10;
A56: DM . hg = hg `11 by A10;
A57: CM . gf = gf `12 by A11;
A58: CM . hg = hg `12 by A11;
A59: DM . gf = f `11 by A53, A55, MCART_1:85;
A60: CM . gf = g `12 by A53, A57, MCART_1:85;
A61: CM . hg = h `12 by A54, A58, MCART_1:85;
A62: [h,gf] in dom CC by A25, A45, A11, A48, A57, A60;
A63: [hg,f] in dom CC by A25, A44, A46, A49, A56, A54, MCART_1:85;
reconsider f9 = f, g9 = g, h9 = h as Element of M ;
A64: P1[f9 `11 ,f9 `12 ,f9 `2 ] by A6;
A65: P1[g9 `11 ,g9 `12 ,g9 `2 ] by A6;
A66: P1[h9 `11 ,h9 `12 ,h9 `2 ] by A6;
A67: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,g) = h (*) g by A33, A48, CAT_1:def 1;
A68: dom (h (*) g) = dom g by A34, A48;
A69: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f) = g (*) f by A33, A49, CAT_1:def 1;
cod (g (*) f) = cod g by A34, A49;
hence h (*) (g (*) f) = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f))) by A69, A33, A48, CAT_1:def 1
.= [[(f `11),(h `12)],F3((h `2),(gf `2))] by A26, A55, A59, A62
.= [[(f `11),(h `12)],F3((h9 `2),F3((g9 `2),(f9 `2)))] by A53
.= [[(f `11),(h `12)],F3(F3((h9 `2),(g9 `2)),(f9 `2))] by A3, A44, A45, A46, A47, A48, A49, A64, A65, A66
.= [[(f `11),(h `12)],F3((hg `2),(f `2))] by A54
.= the Comp of CatStr(# F1(),M,DM,CM,CC #) . (( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,g)),f) by A26, A58, A61, A63
.= (h (*) g) (*) f by A67, A33, A49, A68, CAT_1:def 1 ;
:: thesis: verum
end;
A70: CatStr(# F1(),M,DM,CM,CC #) is reflexive
proof
let b be Object of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}
consider f being Element of F2() such that
A71: I . b = [[b,b],f] and
P1[b,b,f] and
for c being Element of F1()
for g being Element of F2() holds
( ( P1[b,c,g] implies F3(g,f) = g ) & ( P1[c,b,g] implies F3(f,g) = g ) ) by A30;
reconsider bb = b as Element of F1() ;
reconsider Ib = I . bb as Element of M ;
reconsider ii = I . bb as Morphism of CatStr(# F1(),M,DM,CM,CC #) ;
A72: cod ii = (I . b) `12 by A11
.= b by A71, MCART_1:85 ;
dom ii = (I . b) `11 by A10
.= b by A71, MCART_1:85 ;
then I . b in Hom (b,b) by A72;
hence Hom (b,b) <> {} ; :: thesis: verum
end;
CatStr(# F1(),M,DM,CM,CC #) is with_identities
proof
let a be Object of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
consider f being Element of F2() such that
A73: I . a = [[a,a],f] and
P1[a,a,f] and
A74: for c being Element of F1()
for g being Element of F2() holds
( ( P1[a,c,g] implies F3(g,f) = g ) & ( P1[c,a,g] implies F3(f,g) = g ) ) by A30;
reconsider aa = a as Element of F1() ;
reconsider Ia = I . aa as Element of M ;
reconsider ii = I . aa as Morphism of CatStr(# F1(),M,DM,CM,CC #) ;
A75: cod ii = (I . a) `12 by A11
.= a by A73, MCART_1:85 ;
dom ii = (I . a) `11 by A10
.= a by A73, MCART_1:85 ;
then reconsider ii = ii as Morphism of a,a by A75, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of CatStr(# F1(),M,DM,CM,CC #); :: thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A76: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; :: thesis: g (*) ii = g
reconsider bb = b as Element of F1() ;
g in M ;
then consider a1, b1 being Element of F1(), f1 being Element of F2() such that
A77: g = [[a1,b1],f1] and
A78: P1[a1,b1,f1] ;
A79: a = dom g by A76, CAT_1:5
.= DM . g
.= [[a1,b1],f1] `11 by A77, A10
.= a1 by MCART_1:85 ;
then A80: F3(f1,f) = f1 by A74, A78;
A81: [[a,a],f] `11 = a1 by A79, MCART_1:85;
A82: [[a1,b1],f1] `12 = b1 by MCART_1:85;
g `11 = [[a1,b1],f1] `11 by A77
.= a by A79, MCART_1:85
.= [[a,a],f] `12 by MCART_1:85
.= ii `12 by A73 ;
then A83: [g,ii] in dom CC by A25;
hence g (*) ii = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,ii) by CAT_1:def 1
.= CC . (g,ii)
.= [[(ii `11),(g `12)],F3((g `2),(ii `2))] by A26, A83
.= [[a1,b1],f1] by A80, A81, A82, A77, A73
.= g by A77 ;
:: thesis: verum
end;
thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) :: thesis: verum
proof
assume A84: Hom (b,a) <> {} ; :: thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; :: thesis: ii (*) g = g
reconsider bb = b as Element of F1() ;
g in M ;
then consider b1, a1 being Element of F1(), f1 being Element of F2() such that
A85: g = [[b1,a1],f1] and
A86: P1[b1,a1,f1] ;
A87: a = cod g by A84, CAT_1:5
.= CM . g
.= [[b1,a1],f1] `12 by A85, A11
.= a1 by MCART_1:85 ;
then A88: F3(f,f1) = f1 by A74, A86;
A89: [[a,a],f] `12 = a1 by A87, MCART_1:85;
A90: [[b1,a1],f1] `11 = b1 by MCART_1:85;
g `12 = [[b1,a1],f1] `12 by A85
.= a by A87, MCART_1:85
.= [[a,a],f] `11 by MCART_1:85
.= ii `11 by A73 ;
then A91: [ii,g] in dom CC by A25;
hence ii (*) g = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (ii,g) by CAT_1:def 1
.= CC . (ii,g)
.= [[(g `11),(ii `12)],F3((ii `2),(g `2))] by A26, A91
.= [[b1,a1],f1] by A88, A89, A90, A85, A73
.= g by A85 ;
:: thesis: verum
end;
end;
then reconsider C = CatStr(# F1(),M,DM,CM,CC #) as strict Category by A31, A34, A43, A70;
C is with_triple-like_morphisms
proof
let f be Morphism of C; :: according to CAT_5:def 1 :: thesis: ex x being set st f = [[(dom f),(cod f)],x]
f in M ;
then consider a, b being Element of F1(), g being Element of F2() such that
A92: f = [[a,b],g] and
P1[a,b,g] ;
take g ; :: thesis: f = [[(dom f),(cod f)],g]
A93: dom f = f `11 by A10
.= a by A92, MCART_1:85 ;
cod f = f `12 by A11
.= b by A92, MCART_1:85 ;
hence f = [[(dom f),(cod f)],g] by A92, A93; :: thesis: verum
end;
then reconsider C = C as strict with_triple-like_morphisms Category ;
take C ; :: thesis: ( the carrier of C = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) )
thus the carrier of C = F1() ; :: thesis: ( ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) )
hereby :: thesis: ( ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) )
let a, b be Element of F1(); :: thesis: for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C
let f be Element of F2(); :: thesis: ( P1[a,b,f] implies [[a,b],f] is Morphism of C )
assume P1[a,b,f] ; :: thesis: [[a,b],f] is Morphism of C
then [[a,b],f] in M ;
hence [[a,b],f] is Morphism of C ; :: thesis: verum
end;
hereby :: thesis: for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)]
let m be Morphism of C; :: thesis: ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] )
m in M ;
hence ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ; :: thesis: verum
end;
let m1, m2 be Morphism of C; :: thesis: for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)]
let a1, a2, a3 be Element of F1(); :: thesis: for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)]
let f1, f2 be Element of F2(); :: thesis: ( m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] implies m2 (*) m1 = [[a1,a3],F3(f2,f1)] )
assume that
A94: m1 = [[a1,a2],f1] and
A95: m2 = [[a2,a3],f2] ; :: thesis: m2 (*) m1 = [[a1,a3],F3(f2,f1)]
A96: m1 `11 = a1 by A94, MCART_1:85;
A97: m1 `12 = a2 by A94, MCART_1:85;
A98: m2 `11 = a2 by A95, MCART_1:85;
A99: m2 `12 = a3 by A95, MCART_1:85;
thus m2 (*) m1 = CC . (m2,m1) by A25, A97, A98, CAT_1:def 1
.= [[a1,a3],F3((m2 `2),(m1 `2))] by A26, A96, A99, A25, A97, A98
.= [[a1,a3],F3(f2,(m1 `2))] by A95
.= [[a1,a3],F3(f2,f1)] by A94 ; :: thesis: verum