let f be Relation of [:R1,S1:],[:R2,S2:]; :: thesis: ( f = [^R,S^] iff for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) )
thus ( f = [^R,S^] implies for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) ) :: thesis: ( ( for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) ) implies f = [^R,S^] )

proof

assume A1: f = [^R,S^] ; :: thesis: for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )
let r1 be Element of R1; :: thesis: for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )
let r2 be Element of R2; :: thesis: for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )
let s1 be Element of S1; :: thesis: for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )
let s2 be Element of S2; :: thesis: ( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )

hereby :: thesis: ( ( [r1,r2] in R or [s1,s2] in S ) implies [[r1,s1],[r2,s2]] in f )

assume [[r1,s1],[r2,s2]] in f ; :: thesis: ( [r1,r2] in R or [s1,s2] in S )
then consider r1', s1', r2', s2' being set such that
A2: ( [r1,s1] = [r1',s1'] & [r2,s2] = [r2',s2'] ) and
A3: ( r1' in R1 & s1' in S1 & r2' in R2 & s2' in S2 & ( [r1',r2'] in R or [s1',s2'] in S ) ) by A1, Def2;
( r1 = r1' & r2 = r2' & s1 = s1' & s2 = s2' ) by A2, ZFMISC_1:33;
hence ( [r1,r2] in R or [s1,s2] in S ) by A3; :: thesis: verum

end;

thus ( ( [r1,r2] in R or [s1,s2] in S ) implies [[r1,s1],[r2,s2]] in f ) by A1, Def2; :: thesis: verum

end;

assume A4: for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) ; :: thesis: f = [^R,S^]
for x, y being set holds
( [x,y] in f iff [x,y] in [^R,S^] )

proof

let x, y be set ; :: thesis: ( [x,y] in f iff [x,y] in [^R,S^] )
thus ( [x,y] in f implies [x,y] in [^R,S^] ) :: thesis: ( [x,y] in [^R,S^] implies [x,y] in f )

proof

assume A5: [x,y] in f ; :: thesis: [x,y] in [^R,S^]
then x in dom f by RELAT_1:20;
then consider x1, x2 being set such that
A6: ( x1 in R1 & x2 in S1 & x = [x1,x2] ) by ZFMISC_1:def 2;
y in rng f by A5, RELAT_1:20;
then consider y1, y2 being set such that
A7: ( y1 in R2 & y2 in S2 & y = [y1,y2] ) by ZFMISC_1:def 2;
( [x1,y1] in R or [x2,y2] in S ) by A4, A5, A6, A7;
hence [x,y] in [^R,S^] by A6, A7, Def2; :: thesis: verum

end;

assume [x,y] in [^R,S^] ; :: thesis: [x,y] in f
then ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) by Def2;
hence [x,y] in f by A4; :: thesis: verum

end;

hence f = [^R,S^] by RELAT_1:def 2; :: thesis: verum