consider R being ManySortedSet of such that
A2: for i being set st i in F₁() holds
R . i = F₃(i) from PBOOLE:sch 4();
R is ManySortedRelation of F₂()

proof

let i be set ; :: according to MSUALG_4:def 2 :: thesis: ( not i in F₁() or R . i is Element of bool [:(F₂() . i),(F₂() . i):] )
assume i in F₁() ; :: thesis: R . i is Element of bool [:(F₂() . i),(F₂() . i):]
then ( F₃(i) is Relation of (F₂() . i),(F₂() . i) & R . i = F₃(i) ) by A1, A2;
hence R . i is Element of bool [:(F₂() . i),(F₂() . i):] ; :: thesis: verum

end;

hence ex R being ManySortedRelation of F₂() st
for i being set st i in F₁() holds
R . i = F₃(i) by A2; :: thesis: for R1, R2 being ManySortedRelation of F₂() st ( for i being set st i in F₁() holds
R1 . i = F₃(i) ) & ( for i being set st i in F₁() holds
R2 . i = F₃(i) ) holds
R1 = R2
let R1, R2 be ManySortedRelation of F₂(); :: thesis: ( ( for i being set st i in F₁() holds
R1 . i = F₃(i) ) & ( for i being set st i in F₁() holds
R2 . i = F₃(i) ) implies R1 = R2 )
assume that
A3: for i being set st i in F₁() holds
R1 . i = F₃(i) and
A4: for i being set st i in F₁() holds
R2 . i = F₃(i) ; :: thesis: R1 = R2

now

let i be set ; :: thesis: ( i in F₁() implies R1 . i = R2 . i )
assume i in F₁() ; :: thesis: R1 . i = R2 . i
then ( R1 . i = F₃(i) & R2 . i = F₃(i) ) by A3, A4;
hence R1 . i = R2 . i ; :: thesis: verum

end;

hence R1 = R2 by PBOOLE:3; :: thesis: verum