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)
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;

then reconsider f2 = f as ManySortedRelation of A,B by MSUALG_4:def 2;
take f ; :: thesis: ( f is ManySortedRelation of A,B & f is os-compatible )
for s1, s2 being Element of R st s1 <= s2 holds
for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )

proof

let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume s1 <= s2 ; :: thesis: for x, y being set st x in A . s1 & y in B . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
let x, y be set ; :: thesis: ( x in A . s1 & y in B . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that
x in A . s1 and
y in B . s1 ; :: thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
f . s1 = R1 by FUNCOP_1:13
.= f . s2 by FUNCOP_1:13 ;
hence ( [x,y] in f . s1 iff [x,y] in f . s2 ) ; :: thesis: verum

end;

then f2 is os-compatible by Def1;
hence ( f is ManySortedRelation of A,B & f is os-compatible ) ; :: thesis: verum