consider R being Relation such that
A1: R = {} ;
set f = I --> R;
( dom (I --> R) = I & ( for x being set st x in I holds
(I --> R) . x = R ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider f = I --> R as ManySortedSet of I by PBOOLE:def 3;
take f ; :: thesis: for i being set st i in I holds
f . i is Relation of A . i,B . i
for i being set st i in I holds
f . i is Relation of A . i,B . i

proof

let i be set ; :: thesis: ( i in I implies f . i is Relation of A . i,B . i )
assume i in I ; :: thesis: f . i is Relation of A . i,B . i
then f . i = {} by A1, FUNCOP_1:13;
hence f . i is Relation of A . i,B . i by RELSET_1:25; :: thesis: verum

end;

hence for i being set st i in I holds
f . i is Relation of A . i,B . i ; :: thesis: verum