let C1, C2 be strict with_triple-like_morphisms Category; :: thesis: ( the carrier of C1 = 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 C1 ) & ( for m being Morphism of C1 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 C1
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)] ) & the carrier of C2 = 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 C2 ) & ( for m being Morphism of C2 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 C2
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)] ) implies C1 = C2 )
assume that
A1: the carrier of C1 = F1() and
A2: 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 C1 and
A3: for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) and
A4: for m1, m2 being Morphism of C1
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)] and
A5: the carrier of C2 = F1() and
A6: 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 C2 and
A7: for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) and
A8: for m1, m2 being Morphism of C2
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)] ; :: thesis: C1 = C2
A9: the carrier' of C1 = the carrier' of C2
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier' of C2 c= the carrier' of C1
let x be object ; :: thesis: ( x in the carrier' of C1 implies x in the carrier' of C2 )
assume x in the carrier' of C1 ; :: thesis: x in the carrier' of C2
then ex a, b being Element of F1() ex f being Element of F2() st
( x = [[a,b],f] & P1[a,b,f] ) by A3;
then x is Morphism of C2 by A6;
hence x in the carrier' of C2 ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of C2 or x in the carrier' of C1 )
assume x in the carrier' of C2 ; :: thesis: x in the carrier' of C1
then ex a, b being Element of F1() ex f being Element of F2() st
( x = [[a,b],f] & P1[a,b,f] ) by A7;
then x is Morphism of C1 by A2;
hence x in the carrier' of C1 ; :: thesis: verum
end;
A10: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A11: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1;
A12: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A13: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1;
A14: now :: thesis: for x being object st x in the carrier' of C1 holds
the Source of C1 . x = the Source of C2 . x
let x be object ; :: thesis: ( x in the carrier' of C1 implies the Source of C1 . x = the Source of C2 . x )
assume x in the carrier' of C1 ; :: thesis: the Source of C1 . x = the Source of C2 . x
then reconsider m1 = x as Morphism of C1 ;
reconsider m2 = m1 as Morphism of C2 by A9;
thus the Source of C1 . x = dom m1
.= m1 `11 by Th2
.= dom m2 by Th2
.= the Source of C2 . x ; :: thesis: verum
end;
then A15: the Source of C1 = the Source of C2 by A9, A10, A11;
now :: thesis: for x being object st x in the carrier' of C1 holds
the Target of C1 . x = the Target of C2 . x
let x be object ; :: thesis: ( x in the carrier' of C1 implies the Target of C1 . x = the Target of C2 . x )
assume x in the carrier' of C1 ; :: thesis: the Target of C1 . x = the Target of C2 . x
then reconsider m1 = x as Morphism of C1 ;
reconsider m2 = m1 as Morphism of C2 by A9;
thus the Target of C1 . x = cod m1
.= m1 `12 by Th2
.= cod m2 by Th2
.= the Target of C2 . x ; :: thesis: verum
end;
then A16: the Target of C1 = the Target of C2 by A9, A12, A13;
A17: dom the Comp of C1 = dom the Comp of C2
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom the Comp of C2 c= dom the Comp of C1
let x be object ; :: thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 )
assume A18: x in dom the Comp of C1 ; :: thesis: x in dom the Comp of C2
then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] ;
reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A9;
A19: y = [(xx `1),(xx `2)] by MCART_1:21;
then dom (xx `1) = cod (xx `2) by A18, CAT_1:def 6;
then dom (y `1) = cod (y `2) by A14, A16;
hence x in dom the Comp of C2 by A19, CAT_1:def 6; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 )
assume A20: x in dom the Comp of C2 ; :: thesis: x in dom the Comp of C1
then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] by A9;
reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A9;
A21: xx = [(y `1),(y `2)] by MCART_1:21;
then dom (y `1) = cod (y `2) by A20, CAT_1:def 6;
then dom (xx `1) = cod (xx `2) by A14, A16;
hence x in dom the Comp of C1 by A21, CAT_1:def 6; :: thesis: verum
end;
now :: thesis: for x, y being object st [x,y] in dom the Comp of C1 holds
the Comp of C1 . (x,y) = the Comp of C2 . (x,y)
let x, y be object ; :: thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) )
assume A22: [x,y] in dom the Comp of C1 ; :: thesis: the Comp of C1 . (x,y) = the Comp of C2 . (x,y)
then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A9;
consider a1, b1 being Element of F1(), f1 being Element of F2() such that
A23: g1 = [[a1,b1],f1] and
P1[a1,b1,f1] by A3;
consider c1, d1 being Element of F1(), i1 being Element of F2() such that
A24: h1 = [[c1,d1],i1] and
P1[c1,d1,i1] by A3;
A25: a1 = g1 `11 by A23, MCART_1:85
.= dom g1 by Th2
.= cod h1 by A22, CAT_1:15
.= h1 `12 by Th2
.= d1 by A24, MCART_1:85 ;
thus the Comp of C1 . (x,y) = g1 (*) h1 by A22, CAT_1:def 1
.= [[c1,b1],F3(f1,i1)] by A4, A23, A24, A25
.= g2 (*) h2 by A8, A23, A24, A25
.= the Comp of C2 . (x,y) by A17, A22, CAT_1:def 1 ; :: thesis: verum
end;
hence C1 = C2 by A1, A5, A9, A15, A16, A17, BINOP_1:20; :: thesis: verum