let N be set ; :: thesis: for f being Function of N,(bool N) ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i
let f be Function of N,(bool N); :: thesis: ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i
deffunc H₁( set ) -> set = f . $1;
A1: for i being Element of N st i in [#] N holds
H₁(i) c= [#] N

proof

let i be Element of N; :: thesis: ( i in [#] N implies H₁(i) c= [#] N )
assume i in [#] N ; :: thesis: H₁(i) c= [#] N
then f . i in bool N by Th5;
hence H₁(i) c= [#] N ; :: thesis: verum

end;

consider R being Relation of ([#] N) such that
A2: for i being Element of N st i in [#] N holds
Im (R,i) = H₁(i) from RELSET_1:sch 3(A1);
reconsider R = R as Relation of N ;
take R ; :: thesis: for i being set st i in N holds
Im (R,i) = f . i
thus for i being set st i in N holds
Im (R,i) = f . i by A2; :: thesis: verum