consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) ) from RELAT_1:sch 1();
R c= [:F₁(),F₂():]

proof

let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in R or [x1,x2] in [:F₁(),F₂():] )
assume [x1,x2] in R ; :: thesis: [x1,x2] in [:F₁(),F₂():]
then ( x1 in F₁() & x2 in F₂() ) by A1;
hence [x1,x2] in [:F₁(),F₂():] by ZFMISC_1:106; :: thesis: verum

end;

then reconsider R = R as Relation of F₁(),F₂() ;
take R ; :: thesis: for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )
thus for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) ) by A1; :: thesis: verum