defpred S₁[ object , object ] means $2 in F₃($1);
consider R being Relation of F₂() such that
A2: for x, y being object holds
( [x,y] in R iff ( x in F₂() & y in F₂() & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis: for i being Element of F₁() st i in F₂() holds
Im (R,i) = F₃(i)
let i be Element of F₁(); :: thesis: ( i in F₂() implies Im (R,i) = F₃(i) )
assume A3: i in F₂() ; :: thesis: Im (R,i) = F₃(i)
thus Im (R,i) c= F₃(i) :: according to XBOOLE_0:def 10 :: thesis: F₃(i) c= Im (R,i)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Im (R,i) or e in F₃(i) )
assume e in Im (R,i) ; :: thesis: e in F₃(i)
then consider u being object such that
A4: [u,e] in R and
A5: u in {i} by RELAT_1:def 13;
u = i by A5, TARSKI:def 1;
hence e in F₃(i) by A2, A4; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F₃(i) or e in Im (R,i) )
assume A6: e in F₃(i) ; :: thesis: e in Im (R,i)
F₃(i) c= F₂() by A1, A3;
then ( i in {i} & [i,e] in R ) by A2, A3, A6, TARSKI:def 1;
hence e in Im (R,i) by RELAT_1:def 13; :: thesis: verum