thus dom [^R,S^] c= [:R1,S1:] ; :: according to PARTFUN1:def 2,XBOOLE_0:def 10 :: thesis: [:R1,S1:] c= dom [^R,S^]
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:R1,S1:] or z in dom [^R,S^] )
assume z in [:R1,S1:] ; :: thesis: z in dom [^R,S^]
then consider x, y being set such that
A1: x in R1 and
A2: y in S1 and
A3: z = [x,y] by ZFMISC_1:def 2;
dom R = R1 by PARTFUN1:def 2;
then consider a being set such that
A4: [x,a] in R by A1, RELAT_1:def 4;
dom S = S1 by PARTFUN1:def 2;
then consider b being set such that
A5: [y,b] in S by A2, RELAT_1:def 4;
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 A1, A2, A4, A6, Def2;
hence z in dom [^R,S^] by A3, RELAT_1:def 4; :: thesis: verum