consider R being ManySortedSet of F₁() such that
A2: for i being object 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 1 :: thesis: ( not i in F₁() or R . i is Element of bool [:(F₂() . i),(F₂() . i):] )
assume A3: i in F₁() ; :: thesis: R . i is Element of bool [:(F₂() . i),(F₂() . i):]
then F₃(i) is Relation of (F₂() . i),(F₂() . i) by A1;
hence R . i is Element of bool [:(F₂() . i),(F₂() . i):] by A2, A3; :: thesis: verum

end;

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

now :: thesis: for i being object st i in F₁() holds
R1 . i = R2 . i

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

end;

hence R1 = R2 ; :: thesis: verum