defpred S_{1}[ object , object ] means $2 in F_{3}($1);

consider R being Relation of F_{2}() such that

A2: for x, y being object holds

( [x,y] in R iff ( x in F_{2}() & y in F_{2}() & S_{1}[x,y] ) )
from RELSET_1:sch 1();

take R ; :: thesis: for i being Element of F_{1}() st i in F_{2}() holds

Im (R,i) = F_{3}(i)

let i be Element of F_{1}(); :: thesis: ( i in F_{2}() implies Im (R,i) = F_{3}(i) )

assume A3: i in F_{2}()
; :: thesis: Im (R,i) = F_{3}(i)

thus Im (R,i) c= F_{3}(i)
:: according to XBOOLE_0:def 10 :: thesis: F_{3}(i) c= Im (R,i)_{3}(i) or e in Im (R,i) )

assume A6: e in F_{3}(i)
; :: thesis: e in Im (R,i)

F_{3}(i) c= F_{2}()
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

consider R being Relation of F

A2: for x, y being object holds

( [x,y] in R iff ( x in F

take R ; :: thesis: for i being Element of F

Im (R,i) = F

let i be Element of F

assume A3: i in F

thus Im (R,i) c= F

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Im (R,i) or e in F_{3}(i) )

assume e in Im (R,i) ; :: thesis: e in F_{3}(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_{3}(i)
by A2, A4; :: thesis: verum

end;assume e in Im (R,i) ; :: thesis: e in F

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

assume A6: e in F

F

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