set I = the carrier of R;
consider R1 being Relation such that
A1: R1 = {} ;
set f = the carrier of R --> R1;
reconsider f = the carrier of R --> R1 as ManySortedSet of R ;
set f1 = f;
for i being set st i in the carrier of R holds
f . i is Relation of (A . i),(B . i)
proof
let i be set ; :: thesis: ( i in the carrier of R implies f . i is Relation of (A . i),(B . i) )
assume i in the carrier of R ; :: 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;
then reconsider f2 = f as ManySortedRelation of A,B by MSUALG_4:def 1;
take f ; :: thesis: ( f is ManySortedRelation of A,B & f is os-compatible )
f2 is os-compatible ;
hence ( f is ManySortedRelation of A,B & f is os-compatible ) ; :: thesis: verum