let f be Relation of [:R1,S1:],[:R2,S2:]; ( 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 ) ) )
( ( 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^]
;
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;
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;
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;
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;
( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) )
hereby ( ( [r1,r2] in R or [s1,s2] in S ) implies [[r1,s1],[r2,s2]] in f )
assume
[[r1,s1],[r2,s2]] in f
;
( [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;
verum
end;
thus
( (
[r1,r2] in R or
[s1,s2] in S ) implies
[[r1,s1],[r2,s2]] in f )
by A1, Def2;
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 ) )
; 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 ;
( [x,y] in f iff [x,y] in [^R,S^] )
thus
(
[x,y] in f implies
[x,y] in [^R,S^] )
( [x,y] in [^R,S^] implies [x,y] in f )proof
assume A7:
[x,y] in f
;
[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;
verum
end;
assume
[x,y] in [^R,S^]
;
[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;
verum
end;
hence
f = [^R,S^]
; verum