consider R being Relation such that
A1: R = {} ;
set f = I --> R;
reconsider f = I --> R as ManySortedSet of I ;
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)
f . i = {} by A1;
hence f . i is Relation of (A . i),(B . i) by RELSET_1:12; :: thesis: verum
end;
hence for i being set st i in I holds
f . i is Relation of (A . i),(B . i) ; :: thesis: verum