commaObjs (F,G) = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) }
by A1, Def1;
then
[[c1,d1],f1] in commaObjs (F,G)
by A1;
then reconsider o = [[c1,d1],f1] as Element of commaObjs (F,G) ;
set X = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } ;
A2:
( dom (id d1) = d1 & cod (id d1) = d1 )
;
A3:
( (o `1) `1 = o `11 & (o `1) `2 = o `12 )
by MCART_1:def 14, MCART_1:def 15;
A4:
{ [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } c= [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
proof
let x be
object ;
TARSKI:def 3 ( not x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } or x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] )
assume
x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) }
;
x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
then
ex
g being
Morphism of
C ex
h being
Morphism of
D ex
o1,
o2 being
Element of
commaObjs (
F,
G) st
(
x = [[o1,o2],[g,h]] &
dom g = o1 `11 &
cod g = o2 `11 &
dom h = o1 `12 &
cod h = o2 `12 &
(o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) )
;
hence
x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
;
verum
end;
A5:
( [c1,d1] `2 = d1 & o `2 = f1 )
;
cod f1 = G . d1
by A1, CAT_1:1;
then A6:
(id (G . d1)) (*) f1 = f1
by CAT_1:21;
dom f1 = F . c1
by A1, CAT_1:1;
then A7:
f1 (*) (id (F . c1)) = f1
by CAT_1:22;
A8:
( F . (id c1) = id (F . c1) & G . (id d1) = id (G . d1) )
by CAT_1:71;
( dom (id c1) = c1 & cod (id c1) = c1 )
;
then
[[o,o],[(id c1),(id d1)]] in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) }
by A2, A3, A5, A7, A6, A8;
hence
{ [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } is non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:]
by A4; verum