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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ) } ; :: thesis: 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:]:] ; :: thesis: 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; :: thesis: verum