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, Def5;
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 ) by CAT_1:44;
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 set ; :: 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 ) by MCART_1:7;
A6: ( o `1 = [c1,d1] & [c1,d1] `1 = c1 ) by MCART_1:7;
cod f1 = G . d1 by A1, CAT_1:18;
then A7: (id (G . d1)) * f1 = f1 by CAT_1:46;
dom f1 = F . c1 by A1, CAT_1:18;
then A8: f1 * (id (F . c1)) = f1 by CAT_1:47;
A9: ( F . (id c1) = id (F . c1) & G . (id d1) = id (G . d1) ) by CAT_1:108;
( dom (id c1) = c1 & cod (id c1) = c1 ) by CAT_1:44;
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, A6, A5, A8, A7, A9;
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