set O = [:the carrier of C,the carrier of D:];
set M = [:the carrier' of C,the carrier' of D:];
set d = [:the Source of C,the Source of D:];
set c = [:the Target of C,the Target of D:];
set p = |:the Comp of C,the Comp of D:|;
set i = [:the Id of C,the Id of D:];
A1:
for f, g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f holds
( [(g `1 ),(f `1 )] in dom the Comp of C & [(g `2 ),(f `2 )] in dom the Comp of D )
proof
let f,
g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f implies ( [(g `1 ),(f `1 )] in dom the Comp of C & [(g `2 ),(f `2 )] in dom the Comp of D ) )
A2:
(
g = [(g `1 ),(g `2 )] &
f = [(f `1 ),(f `2 )] )
by MCART_1:23;
A3:
(
[:the Source of C,the Source of D:] . (g `1 ),
(g `2 ) = [(the Source of C . (g `1 )),(the Source of D . (g `2 ))] &
[:the Target of C,the Target of D:] . (f `1 ),
(f `2 ) = [(the Target of C . (f `1 )),(the Target of D . (f `2 ))] )
by FUNCT_3:96;
assume
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
;
:: thesis: ( [(g `1 ),(f `1 )] in dom the Comp of C & [(g `2 ),(f `2 )] in dom the Comp of D )
then
( the
Source of
C . (g `1 ) = the
Target of
C . (f `1 ) & the
Source of
D . (g `2 ) = the
Target of
D . (f `2 ) )
by A2, A3, ZFMISC_1:33;
hence
(
[(g `1 ),(f `1 )] in dom the
Comp of
C &
[(g `2 ),(f `2 )] in dom the
Comp of
D )
by CAT_1:def 8;
:: thesis: verum
end;
A4:
for f, g being Element of [:the carrier' of C,the carrier' of D:] st [g,f] in dom |:the Comp of C,the Comp of D:| holds
( the Source of C . (g `1 ) = the Target of C . (f `1 ) & the Source of D . (g `2 ) = the Target of D . (f `2 ) )
proof
let f,
g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [g,f] in dom |:the Comp of C,the Comp of D:| implies ( the Source of C . (g `1 ) = the Target of C . (f `1 ) & the Source of D . (g `2 ) = the Target of D . (f `2 ) ) )
A5:
(
g = [(g `1 ),(g `2 )] &
f = [(f `1 ),(f `2 )] )
by MCART_1:23;
assume
[g,f] in dom |:the Comp of C,the Comp of D:|
;
:: thesis: ( the Source of C . (g `1 ) = the Target of C . (f `1 ) & the Source of D . (g `2 ) = the Target of D . (f `2 ) )
then
(
[(g `1 ),(f `1 )] in dom the
Comp of
C &
[(g `2 ),(f `2 )] in dom the
Comp of
D )
by A5, FUNCT_4:57;
hence
( the
Source of
C . (g `1 ) = the
Target of
C . (f `1 ) & the
Source of
D . (g `2 ) = the
Target of
D . (f `2 ) )
by CAT_1:def 8;
:: thesis: verum
end;
A6:
for f, g being Element of [:the carrier' of C,the carrier' of D:] holds
( [g,f] in dom |:the Comp of C,the Comp of D:| iff [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f )
proof
let f,
g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [g,f] in dom |:the Comp of C,the Comp of D:| iff [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f )
A7:
(
g = [(g `1 ),(g `2 )] &
f = [(f `1 ),(f `2 )] )
by MCART_1:23;
thus
(
[g,f] in dom |:the Comp of C,the Comp of D:| implies
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f )
:: thesis: ( [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f implies [g,f] in dom |:the Comp of C,the Comp of D:| )proof
assume
[g,f] in dom |:the Comp of C,the Comp of D:|
;
:: thesis: [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
then
( the
Source of
C . (g `1 ) = the
Target of
C . (f `1 ) & the
Source of
D . (g `2 ) = the
Target of
D . (f `2 ) &
[:the Source of C,the Source of D:] . (g `1 ),
(g `2 ) = [(the Source of C . (g `1 )),(the Source of D . (g `2 ))] &
[:the Target of C,the Target of D:] . (f `1 ),
(f `2 ) = [(the Target of C . (f `1 )),(the Target of D . (f `2 ))] )
by A4, FUNCT_3:96;
hence
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
by A7;
:: thesis: verum
end;
assume
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
;
:: thesis: [g,f] in dom |:the Comp of C,the Comp of D:|
then
(
[(g `1 ),(f `1 )] in dom the
Comp of
C &
[(g `2 ),(f `2 )] in dom the
Comp of
D )
by A1;
hence
[g,f] in dom |:the Comp of C,the Comp of D:|
by A7, FUNCT_4:57;
:: thesis: verum
end;
A8:
for f, g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f holds
|:the Comp of C,the Comp of D:| . g,f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))]
proof
let f,
g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f implies |:the Comp of C,the Comp of D:| . g,f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))] )
assume
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
;
:: thesis: |:the Comp of C,the Comp of D:| . g,f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))]
then
(
[g,f] in dom |:the Comp of C,the Comp of D:| &
g = [(g `1 ),(g `2 )] &
f = [(f `1 ),(f `2 )] )
by A6, MCART_1:23;
hence
|:the Comp of C,the Comp of D:| . g,
f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))]
by FUNCT_4:58;
:: thesis: verum
end;
A9:
for f, g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f holds
( [:the Source of C,the Source of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Source of C,the Source of D:] . f & [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Target of C,the Target of D:] . g )
proof
let f,
g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f implies ( [:the Source of C,the Source of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Source of C,the Source of D:] . f & [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Target of C,the Target of D:] . g ) )
A10:
(
g = [(g `1 ),(g `2 )] &
f = [(f `1 ),(f `2 )] )
by MCART_1:23;
A11:
(
[:the Source of C,the Source of D:] . (f `1 ),
(f `2 ) = [(the Source of C . (f `1 )),(the Source of D . (f `2 ))] &
[:the Target of C,the Target of D:] . (g `1 ),
(g `2 ) = [(the Target of C . (g `1 )),(the Target of D . (g `2 ))] )
by FUNCT_3:96;
assume A12:
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f
;
:: thesis: ( [:the Source of C,the Source of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Source of C,the Source of D:] . f & [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Target of C,the Target of D:] . g )
then A13:
[g,f] in dom |:the Comp of C,the Comp of D:|
by A6;
(
[(g `1 ),(f `1 )] in dom the
Comp of
C &
[(g `2 ),(f `2 )] in dom the
Comp of
D )
by A1, A12;
then
( the
Source of
C . (g `1 ) = the
Target of
C . (f `1 ) & the
Source of
D . (g `2 ) = the
Target of
D . (f `2 ) & the
Comp of
C . [(g `1 ),(f `1 )] in the
carrier' of
C & the
Comp of
D . [(g `2 ),(f `2 )] in the
carrier' of
D )
by A4, A13, PARTFUN1:27;
then A14:
( the
Source of
C . (the Comp of C . (g `1 ),(f `1 )) = the
Source of
C . (f `1 ) & the
Source of
D . (the Comp of D . (g `2 ),(f `2 )) = the
Source of
D . (f `2 ) & the
Target of
C . (the Comp of C . (g `1 ),(f `1 )) = the
Target of
C . (g `1 ) & the
Target of
D . (the Comp of D . (g `2 ),(f `2 )) = the
Target of
D . (g `2 ) & the
Comp of
C . (g `1 ),
(f `1 ) in dom the
Source of
C & the
Comp of
D . (g `2 ),
(f `2 ) in dom the
Source of
D & the
Comp of
C . (g `1 ),
(f `1 ) in dom the
Target of
C & the
Comp of
D . (g `2 ),
(f `2 ) in dom the
Target of
D &
|:the Comp of C,the Comp of D:| . g,
f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))] )
by A8, A12, CAT_1:def 8, FUNCT_2:def 1;
thus [:the Source of C,the Source of D:] . (|:the Comp of C,the Comp of D:| . g,f) =
[:the Source of C,the Source of D:] . (the Comp of C . (g `1 ),(f `1 )),
(the Comp of D . (g `2 ),(f `2 ))
by A8, A12
.=
[:the Source of C,the Source of D:] . f
by A10, A11, A14, FUNCT_3:def 9
;
:: thesis: [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) = [:the Target of C,the Target of D:] . g
thus [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) =
[:the Target of C,the Target of D:] . (the Comp of C . (g `1 ),(f `1 )),
(the Comp of D . (g `2 ),(f `2 ))
by A8, A12
.=
[:the Target of C,the Target of D:] . g
by A10, A11, A14, FUNCT_3:def 9
;
:: thesis: verum
end;
A15:
for f, g, h being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . h = [:the Target of C,the Target of D:] . g & [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f holds
|:the Comp of C,the Comp of D:| . h,(|:the Comp of C,the Comp of D:| . g,f) = |:the Comp of C,the Comp of D:| . (|:the Comp of C,the Comp of D:| . h,g),f
proof
let f,
g,
h be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Source of C,the Source of D:] . h = [:the Target of C,the Target of D:] . g & [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f implies |:the Comp of C,the Comp of D:| . h,(|:the Comp of C,the Comp of D:| . g,f) = |:the Comp of C,the Comp of D:| . (|:the Comp of C,the Comp of D:| . h,g),f )
assume A16:
(
[:the Source of C,the Source of D:] . h = [:the Target of C,the Target of D:] . g &
[:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f )
;
:: thesis: |:the Comp of C,the Comp of D:| . h,(|:the Comp of C,the Comp of D:| . g,f) = |:the Comp of C,the Comp of D:| . (|:the Comp of C,the Comp of D:| . h,g),f
then A17:
(
[(g `1 ),(f `1 )] in dom the
Comp of
C &
[(g `2 ),(f `2 )] in dom the
Comp of
D &
[(h `1 ),(g `1 )] in dom the
Comp of
C &
[(h `2 ),(g `2 )] in dom the
Comp of
D )
by A1;
then
( the
Comp of
C . [(g `1 ),(f `1 )] in the
carrier' of
C & the
Comp of
D . [(g `2 ),(f `2 )] in the
carrier' of
D & the
Comp of
C . [(h `1 ),(g `1 )] in the
carrier' of
C & the
Comp of
D . [(h `2 ),(g `2 )] in the
carrier' of
D )
by PARTFUN1:27;
then reconsider pgf =
[(the Comp of C . [(g `1 ),(f `1 )]),(the Comp of D . [(g `2 ),(f `2 )])],
phg =
[(the Comp of C . [(h `1 ),(g `1 )]),(the Comp of D . [(h `2 ),(g `2 )])] as
Element of
[:the carrier' of C,the carrier' of D:] by ZFMISC_1:106;
A18:
(
pgf `1 = the
Comp of
C . [(g `1 ),(f `1 )] &
pgf `2 = the
Comp of
D . [(g `2 ),(f `2 )] &
phg `1 = the
Comp of
C . [(h `1 ),(g `1 )] &
phg `2 = the
Comp of
D . [(h `2 ),(g `2 )] )
by MCART_1:7;
set pgf1 =
pgf `1 ;
set phg1 =
phg `1 ;
set pgf2 =
pgf `2 ;
set phg2 =
phg `2 ;
A19:
( the
Source of
C . (g `1 ) = the
Target of
C . (f `1 ) & the
Source of
D . (g `2 ) = the
Target of
D . (f `2 ) & the
Source of
C . (h `1 ) = the
Target of
C . (g `1 ) & the
Source of
D . (h `2 ) = the
Target of
D . (g `2 ) )
by A17, CAT_1:def 8;
A20:
|:the Comp of C,the Comp of D:| . g,
f = [(the Comp of C . (g `1 ),(f `1 )),(the Comp of D . (g `2 ),(f `2 ))]
by A8, A16;
A21:
|:the Comp of C,the Comp of D:| . h,
g = [(the Comp of C . (h `1 ),(g `1 )),(the Comp of D . (h `2 ),(g `2 ))]
by A8, A16;
(
[:the Source of C,the Source of D:] . h = [:the Target of C,the Target of D:] . (|:the Comp of C,the Comp of D:| . g,f) &
[:the Source of C,the Source of D:] . (|:the Comp of C,the Comp of D:| . h,g) = [:the Target of C,the Target of D:] . f )
by A9, A16;
then
(
|:the Comp of C,the Comp of D:| . h,
(|:the Comp of C,the Comp of D:| . g,f) = [(the Comp of C . (h `1 ),(pgf `1 )),(the Comp of D . (h `2 ),(pgf `2 ))] &
|:the Comp of C,the Comp of D:| . (|:the Comp of C,the Comp of D:| . h,g),
f = [(the Comp of C . (phg `1 ),(f `1 )),(the Comp of D . (phg `2 ),(f `2 ))] & the
Comp of
C . (h `1 ),
(pgf `1 ) = the
Comp of
C . (phg `1 ),
(f `1 ) & the
Comp of
D . (h `2 ),
(pgf `2 ) = the
Comp of
D . (phg `2 ),
(f `2 ) )
by A8, A18, A19, A20, A21, CAT_1:def 8;
hence
|:the Comp of C,the Comp of D:| . h,
(|:the Comp of C,the Comp of D:| . g,f) = |:the Comp of C,the Comp of D:| . (|:the Comp of C,the Comp of D:| . h,g),
f
;
:: thesis: verum
end;
now let b be
Element of
[:the carrier of C,the carrier of D:];
:: thesis: ( [:the Source of C,the Source of D:] . ([:the Id of C,the Id of D:] . b) = b & [:the Target of C,the Target of D:] . ([:the Id of C,the Id of D:] . b) = b & ( for f being Element of [:the carrier' of C,the carrier' of D:] st [:the Target of C,the Target of D:] . f = b holds
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),f = f ) & ( for g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = b holds
|:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = g ) )A22:
b = [(b `1 ),(b `2 )]
by MCART_1:23;
A23:
( the
Source of
C . (the Id of C . (b `1 )) = b `1 & the
Source of
D . (the Id of D . (b `2 )) = b `2 & the
Target of
C . (the Id of C . (b `1 )) = b `1 & the
Target of
D . (the Id of D . (b `2 )) = b `2 &
[:the Id of C,the Id of D:] . (b `1 ),
(b `2 ) = [(the Id of C . (b `1 )),(the Id of D . (b `2 ))] )
by CAT_1:def 8, FUNCT_3:96;
hence A24:
[:the Source of C,the Source of D:] . ([:the Id of C,the Id of D:] . b) =
[:the Source of C,the Source of D:] . (the Id of C . (b `1 )),
(the Id of D . (b `2 ))
by MCART_1:23
.=
b
by A22, A23, FUNCT_3:96
;
:: thesis: ( [:the Target of C,the Target of D:] . ([:the Id of C,the Id of D:] . b) = b & ( for f being Element of [:the carrier' of C,the carrier' of D:] st [:the Target of C,the Target of D:] . f = b holds
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),f = f ) & ( for g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = b holds
|:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = g ) )thus A25:
[:the Target of C,the Target of D:] . ([:the Id of C,the Id of D:] . b) =
[:the Target of C,the Target of D:] . (the Id of C . (b `1 )),
(the Id of D . (b `2 ))
by A23, MCART_1:23
.=
b
by A22, A23, FUNCT_3:96
;
:: thesis: ( ( for f being Element of [:the carrier' of C,the carrier' of D:] st [:the Target of C,the Target of D:] . f = b holds
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),f = f ) & ( for g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = b holds
|:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = g ) )A26:
(
([:the Id of C,the Id of D:] . (b `1 ),(b `2 )) `1 = the
Id of
C . (b `1 ) &
([:the Id of C,the Id of D:] . (b `1 ),(b `2 )) `2 = the
Id of
D . (b `2 ) )
by A23, MCART_1:7;
thus
for
f being
Element of
[:the carrier' of C,the carrier' of D:] st
[:the Target of C,the Target of D:] . f = b holds
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),
f = f
:: thesis: for g being Element of [:the carrier' of C,the carrier' of D:] st [:the Source of C,the Source of D:] . g = b holds
|:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = gproof
let f be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Target of C,the Target of D:] . f = b implies |:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),f = f )
A27:
f = [(f `1 ),(f `2 )]
by MCART_1:23;
assume A28:
[:the Target of C,the Target of D:] . f = b
;
:: thesis: |:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),f = f
[:the Target of C,the Target of D:] . (f `1 ),
(f `2 ) = [(the Target of C . (f `1 )),(the Target of D . (f `2 ))]
by FUNCT_3:96;
then
( the
Target of
C . (f `1 ) = b `1 & the
Target of
D . (f `2 ) = b `2 )
by A22, A27, A28, ZFMISC_1:33;
then
(
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . (b `1 ),(b `2 )),
f = [(the Comp of C . (([:the Id of C,the Id of D:] . b) `1 ),(f `1 )),(the Comp of D . (([:the Id of C,the Id of D:] . b) `2 ),(f `2 ))] & the
Comp of
C . (the Id of C . (b `1 )),
(f `1 ) = f `1 & the
Comp of
D . (the Id of D . (b `2 )),
(f `2 ) = f `2 )
by A8, A22, A24, A28, CAT_1:def 8;
hence
|:the Comp of C,the Comp of D:| . ([:the Id of C,the Id of D:] . b),
f = f
by A22, A26, MCART_1:23;
:: thesis: verum
end; let g be
Element of
[:the carrier' of C,the carrier' of D:];
:: thesis: ( [:the Source of C,the Source of D:] . g = b implies |:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = g )A29:
g = [(g `1 ),(g `2 )]
by MCART_1:23;
assume A30:
[:the Source of C,the Source of D:] . g = b
;
:: thesis: |:the Comp of C,the Comp of D:| . g,([:the Id of C,the Id of D:] . b) = g
[:the Source of C,the Source of D:] . (g `1 ),
(g `2 ) = [(the Source of C . (g `1 )),(the Source of D . (g `2 ))]
by FUNCT_3:96;
then
( the
Source of
C . (g `1 ) = b `1 & the
Source of
D . (g `2 ) = b `2 )
by A22, A29, A30, ZFMISC_1:33;
then
(
|:the Comp of C,the Comp of D:| . g,
([:the Id of C,the Id of D:] . (b `1 ),(b `2 )) = [(the Comp of C . (g `1 ),(([:the Id of C,the Id of D:] . b) `1 )),(the Comp of D . (g `2 ),(([:the Id of C,the Id of D:] . b) `2 ))] & the
Comp of
C . (g `1 ),
(the Id of C . (b `1 )) = g `1 & the
Comp of
D . (g `2 ),
(the Id of D . (b `2 )) = g `2 )
by A8, A22, A25, A30, CAT_1:def 8;
hence
|:the Comp of C,the Comp of D:| . g,
([:the Id of C,the Id of D:] . b) = g
by A22, A26, MCART_1:23;
:: thesis: verum end;
hence
CatStr(# [:the carrier of C,the carrier of D:],[:the carrier' of C,the carrier' of D:],[:the Source of C,the Source of D:],[:the Target of C,the Target of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #) is Category
by A6, A9, A15, CAT_1:def 8; :: thesis: verum