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 r19, s19, r29, s29 being set such that
A2: [r1,s1] = [r19,s19] and
A3: [r2,s2] = [r29,s29] and
r19 in R1 and
s19 in S1 and
r29 in R2 and
s29 in S2 and
A4: ( [r19,r29] in R or [s19,s29] in S ) by A1, Def2;
A5: r1 = r19 by A2, XTUPLE_0:1;
s1 = s19 by A2, XTUPLE_0:1;
hence ( [r1,r2] in R or [s1,s2] in S ) by A3, A4, A5, XTUPLE_0:1; :: 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 A6: 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 object holds
( [x,y] in f iff [x,y] in [^R,S^] )
proof
let x, y be object ; :: 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 A7: [x,y] in f ; :: thesis: [x,y] in [^R,S^]
then x in dom f by XTUPLE_0:def 12;
then consider x1, x2 being object such that
A8: x1 in R1 and
A9: x2 in S1 and
A10: x = [x1,x2] by ZFMISC_1:def 2;
y in rng f by A7, XTUPLE_0:def 13;
then consider y1, y2 being object such that
A11: y1 in R2 and
A12: y2 in S2 and
A13: y = [y1,y2] by ZFMISC_1:def 2;
( [x1,y1] in R or [x2,y2] in S ) by A6, A7, A8, A9, A10, A11, A12, A13;
hence [x,y] in [^R,S^] by A8, A9, A10, A11, A12, A13, 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 A6; :: thesis: verum
end;
hence f = [^R,S^] ; :: thesis: verum