let x, y be object ; :: according to RELAT_1:def 2,PARTFUN1:def 2 :: thesis: ( ( not [^,^] in dom [^R,S^] or [^,^] in [:R1,S1:] ) & ( not [^,^] in [:R1,S1:] or [^,^] in dom [^R,S^] ) )
thus ( [x,y] in dom [^R,S^] implies [x,y] in [:R1,S1:] ) ; :: thesis: ( not [^,^] in [:R1,S1:] or [^,^] in dom [^R,S^] )
assume A1: [x,y] in [:R1,S1:] ; :: thesis: [^,^] in dom [^R,S^]
then A2: x in R1 by ZFMISC_1:87;
A3: y in S1 by A1, ZFMISC_1:87;
dom R = R1 by PARTFUN1:def 2;
then consider a being object such that
A4: [x,a] in R by A2, XTUPLE_0:def 12;
dom S = S1 by PARTFUN1:def 2;
then consider b being object such that
A5: [y,b] in S by A3, XTUPLE_0:def 12;
A6: a in R1 by A4, ZFMISC_1:87;
b in S1 by A5, ZFMISC_1:87;
then [[x,y],[a,b]] in [^R,S^] by A2, A3, A4, A6, Def2;
hence [^,^] in dom [^R,S^] by XTUPLE_0:def 12; :: thesis: verum