consider R being Relation such that
A1: for x, y being object holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) from RELAT_1:sch 1();
 R c= [:F1(),F2():]
proof
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in R or [x1,x2] in [:F1(),F2():] )
assume [x1,x2] in R ; :: thesis: [x1,x2] in [:F1(),F2():]
then ( x1 in F1() & x2 in F2() ) by A1;
hence [x1,x2] in [:F1(),F2():] by ZFMISC_1:87; :: thesis: verum
end;
then reconsider R = R as Relation of F1(),F2() ;
take R ; :: thesis: for x, y being object holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
thus for x, y being object holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) by A1; :: thesis: verum