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
A2: the carrier of C1 = F1() and
A3: 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
A4: 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
A5: 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
A6: the carrier of C2 = F1() and
A7: 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
A8: 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
A9: 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
A10: 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 set ; :: 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 A4;
then x is Morphism of C2 by A7;
hence x in the carrier' of C2 ; :: thesis: verum
end;
let x be set ; :: 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 A8;
then x is Morphism of C1 by A3;
hence x in the carrier' of C1 ; :: thesis: verum
end;
A11: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A12: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1;
A13: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A14: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1;
A15: dom the Id of C1 = the carrier of C1 by FUNCT_2:def 1;
A16: dom the Id of C2 = the carrier of C2 by FUNCT_2:def 1;
now
let x be set ; :: 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 A10;
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 A17: the Source of C1 = the Source of C2 by A10, A11, A12, FUNCT_1:9;
now
let x be set ; :: 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 A10;
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 A18: the Target of C1 = the Target of C2 by A10, A13, A14, FUNCT_1:9;
now
let x be set ; :: thesis: ( x in F1() implies the Id of C1 . x = the Id of C2 . x )
assume x in F1() ; :: thesis: the Id of C1 . x = the Id of C2 . x
then reconsider a = x as Element of F1() ;
consider f being Element of F2() such that
A19: P1[a,a,f] and
A20: 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 A1;
reconsider o1 = a as Object of C1 by A2;
consider a1, b1 being Element of F1(), f1 being Element of F2() such that
A21: id o1 = [[a1,b1],f1] and
A22: P1[a1,b1,f1] by A4;
reconsider o2 = a as Object of C2 by A6;
consider a2, b2 being Element of F1(), f2 being Element of F2() such that
A23: id o2 = [[a2,b2],f2] and
A24: P1[a2,b2,f2] by A8;
A25: dom (id o1) = o1 by CAT_1:44;
A26: cod (id o1) = o1 by CAT_1:44;
A27: dom (id o2) = o2 by CAT_1:44;
A28: cod (id o2) = o2 by CAT_1:44;
A29: o1 = (id o1) `11 by A25, Th2;
A30: o1 = (id o1) `12 by A26, Th2;
A31: o2 = (id o2) `11 by A27, Th2;
A32: o2 = (id o2) `12 by A28, Th2;
A33: o1 = a1 by A21, A29, MCART_1:89;
A34: o1 = b1 by A21, A30, MCART_1:89;
A35: o2 = a2 by A23, A31, MCART_1:89;
A36: o2 = b2 by A23, A32, MCART_1:89;
reconsider m1 = [[a,a],f] as Morphism of C1 by A3, A19;
reconsider m2 = [[a,a],f] as Morphism of C2 by A7, A19;
cod m1 = m1 `12 by Th2
.= a by MCART_1:89 ;
then A37: m1 = (id o1) * m1 by CAT_1:46
.= [[a,a],F3(f1,f)] by A5, A21, A33, A34
.= [[a,a],f1] by A20, A22, A33 ;
cod m2 = m2 `12 by Th2
.= a by MCART_1:89 ;
then m2 = (id o2) * m2 by CAT_1:46
.= [[a,a],F3(f2,f)] by A9, A23, A35, A36
.= [[a,a],f2] by A20, A24, A35 ;
hence the Id of C1 . x = the Id of C2 . x by A21, A23, A32, A33, A34, A35, A37, MCART_1:89; :: thesis: verum
end;
then A38: the Id of C1 = the Id of C2 by A2, A6, A15, A16, FUNCT_1:9;
A39: 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 set ; :: thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 )
assume A40: 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 A10;
A41: y = [(xx `1),(xx `2)] by MCART_1:23;
then the Source of C1 . (xx `1) = the Target of C1 . (xx `2) by A40, CAT_1:def 8;
hence x in dom the Comp of C2 by A10, A17, A18, A41, CAT_1:def 8; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 )
assume A42: 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 A10;
reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A10;
A43: xx = [(y `1),(y `2)] by MCART_1:23;
then the Source of C2 . (y `1) = the Target of C2 . (y `2) by A42, CAT_1:def 8;
hence x in dom the Comp of C1 by A10, A17, A18, A43, CAT_1:def 8; :: thesis: verum
end;
now
let x, y be set ; :: thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) )
assume A44: [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:106;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A10;
consider a1, b1 being Element of F1(), f1 being Element of F2() such that
A45: g1 = [[a1,b1],f1] and
P1[a1,b1,f1] by A4;
consider c1, d1 being Element of F1(), i1 being Element of F2() such that
A46: h1 = [[c1,d1],i1] and
P1[c1,d1,i1] by A4;
A47: a1 = g1 `11 by A45, MCART_1:89
.= dom g1 by Th2
.= cod h1 by A44, CAT_1:40
.= h1 `12 by Th2
.= d1 by A46, MCART_1:89 ;
thus the Comp of C1 . (x,y) = g1 * h1 by A44, CAT_1:def 4
.= [[c1,b1],F3(f1,i1)] by A5, A45, A46, A47
.= g2 * h2 by A9, A45, A46, A47
.= the Comp of C2 . (x,y) by A39, A44, CAT_1:def 4 ; :: thesis: verum
end;
hence C1 = C2 by A2, A6, A10, A17, A18, A38, A39, BINOP_1:32; :: thesis: verum