defpred S1[ object , object ] means $2 in F3($1);
consider R being Relation of F2() such that
A2: for x, y being object holds
( [x,y] in R iff ( x in F2() & y in F2() & S1[x,y] ) ) from RELSET_1:sch 1();
 take R ; :: thesis: for i being Element of F1() st i in F2() holds
Im (R,i) = F3(i)
let i be Element of F1(); :: thesis: ( i in F2() implies Im (R,i) = F3(i) )
assume A3: i in F2() ; :: thesis: Im (R,i) = F3(i)
thus Im (R,i) c= F3(i) :: according to XBOOLE_0:def 10 :: thesis: F3(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 F3(i) )
assume e in Im (R,i) ; :: thesis: e in F3(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 F3(i) by A2, A4; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F3(i) or e in Im (R,i) )
assume A6: e in F3(i) ; :: thesis: e in Im (R,i)
F3(i) c= F2() 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