let P, Q be non empty RelStr ; :: thesis: for x being object holds
( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] )
let x be object ; :: thesis: ( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] )
( x in the carrier of [:P,Q:] iff x in [: the carrier of P, the carrier of Q:] ) by YELLOW_3:def 2;
then ( x in the carrier of [:P,Q:] iff ex p, q being object st
( p in the carrier of P & q in the carrier of Q & x = [p,q] ) ) by ZFMISC_1:def 2;
hence ( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] ) ; :: thesis: verum