defpred S1[ object , object ] means ex p, s, q, t being object st
( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R );
consider Q being Relation such that
A1:
for x, y being object holds
( [x,y] in Q iff ( x in [:(dom P),(dom R):] & y in [:(rng P),(rng R):] & S1[x,y] ) )
from RELAT_1:sch 1();
take
Q
; for x, y being object holds
( [x,y] in Q iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
let x, y be object ; ( [x,y] in Q iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
hereby ( ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) implies [x,y] in Q )
assume
[x,y] in Q
;
ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )then consider p,
s,
q,
t being
object such that A2:
(
x = [p,q] &
y = [s,t] &
[p,s] in P &
[q,t] in R )
by A1;
take p =
p;
ex q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )take q =
q;
ex s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )take s =
s;
ex t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )take t =
t;
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )thus
(
x = [p,q] &
y = [s,t] &
[p,s] in P &
[q,t] in R )
by A2;
verum
end;
given p, q, s, t being object such that A3:
x = [p,q]
and
A4:
y = [s,t]
and
A5:
( [p,s] in P & [q,t] in R )
; [x,y] in Q
( s in rng P & t in rng R )
by A5, XTUPLE_0:def 13;
then A6:
y in [:(rng P),(rng R):]
by A4, ZFMISC_1:87;
( p in dom P & q in dom R )
by A5, XTUPLE_0:def 12;
then
x in [:(dom P),(dom R):]
by A3, ZFMISC_1:87;
hence
[x,y] in Q
by A1, A3, A4, A5, A6; verum